Skip to content

Commit ec05634

Browse files
committed
chore(Geometry/Manifold/VectorBundle/SmoothSection): add module deprecation (leanprover-community#39312)
Module `SmoothSection` has been deprecated in favour of `ContMDiffSection` - see leanprover-community#39272.
1 parent ffe06c9 commit ec05634

2 files changed

Lines changed: 11 additions & 0 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4616,6 +4616,7 @@ public import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
46164616
public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
46174617
public import Mathlib.Geometry.Manifold.VectorBundle.Pullback
46184618
public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
4619+
public import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
46194620
public import Mathlib.Geometry.Manifold.VectorBundle.Tangent
46204621
public import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
46214622
public import Mathlib.Geometry.Manifold.VectorField.LieBracket
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
/-
2+
Copyright (c) 2023 Heather Macbeth. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Heather Macbeth, Floris van Doorn, Michael Rothgang
5+
-/
6+
module
7+
8+
public import Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
9+
10+
deprecated_module (since := "2026-05-12")

0 commit comments

Comments
 (0)