Revision #2189 → #2856 · back to history
addedTangent bundleff70b1ebd127
modifiedVector field as section of the tangent bundle79f55b14da8b
| Field | From #2189 | To #2856 |
|---|
| mathlib.module | Mathlib.Geometry.Manifold.VectorBundle.SmoothSection | Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection |
modifiedSmooth/analytic vector fields on manifold1dcf8ca220c0
| Field | From #2189 | To #2856 |
|---|
| mathlib.module | Mathlib.Geometry.Manifold.VectorBundle.SmoothSection | Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection |
addedGradient operator (del)6cde3f86bed9
addedRectifiable curvee2785be9ecba
addedRiemannian manifolde72fb81d6c99
addedExterior derivative (curl generalization)f491f8743ff9
addedStationary point of a vector fieldb58b188df15a
addedPushforward on tangent bundles2fb80a20f4bf
modifiedDifferential k-formf9063b512bcd
| Field | From #2189 | To #2856 |
|---|
| note | Pointwise alternating multilinear maps and exterior derivatives appear in `Mathlib.Analysis.Calculus.DifferentialForm.VectorField`, but global differential k-forms as bundle sections are not packaged as a single definition. | Pointwise alternating multilinear maps (`ContinuousAlternatingMap`) exist, but global differential k-forms as bundle sections are not packaged as a single definition. |