Commit 2023-07-11 09:17 b009280b

View on Github →

feat: port Geometry.Manifold.VectorBundle.Hom (#5727)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/ContMDiff.lean

added theorem ContDiff.comp_contMDiffAt

added theorem ContDiff.comp_contMDiffWithinAt

added theorem ContDiffAt.comp_contMDiffWithinAt

added theorem ContMDiff.cle_arrowCongr

added theorem ContMDiff.clm_postcomp

added theorem ContMDiff.clm_precomp

deleted theorem ContMDiffAt.clm_apply

deleted theorem ContMDiffAt.clm_prodMap

added theorem ContMDiffOn.cle_arrowCongr

added theorem ContMDiffOn.clm_precomp

added theorem ContMDiffWithinAt.cle_arrowCongr

added theorem ContMDiffWithinAt.clm_postcomp

added theorem ContMDiffWithinAt.clm_precomp

added theorem ContinuousLinearMap.contMDiffAt

added theorem ContinuousLinearMap.contMDiffOn

added theorem ContinuousLinearMap.contMDiffWithinAt

added theorem ContinuousLinearMap.smooth

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

added theorem contMDiffAt_hom_bundle

added theorem hom_chart

added theorem smoothAt_hom_bundle

added theorem smoothOn_continuousLinearMapCoordChange