Commit 2023-07-06 08:16 af1edf05

View on Github →

feat: port Geometry.Manifold.VectorBundle.SmoothSection (#5736)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean

added def ContMDiffSection.coeAddHom

added theorem ContMDiffSection.coeFn_mk

added theorem ContMDiffSection.coe_add

added theorem ContMDiffSection.coe_inj

added theorem ContMDiffSection.coe_injective

added theorem ContMDiffSection.coe_neg

added theorem ContMDiffSection.coe_nsmul

added theorem ContMDiffSection.coe_smul

added theorem ContMDiffSection.coe_sub

added theorem ContMDiffSection.coe_zero

added theorem ContMDiffSection.coe_zsmul

added theorem ContMDiffSection.ext

added structure ContMDiffSection

added def SmoothSection