Commit 2026-05-07 17:04 6bd147ba

View on Github →

feat(Geometry/Manifold): add ContMDiffSMul typeclass (#38565) Introduce typeclasses ContMDiffVAdd and ContMDiffSMul for continuously differentiable actions on manifolds. As an application, we prove that the general linear group (V →L[𝕜] V)ˣ of any Banach space V acts smoothly on V.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

Created Mathlib/Geometry/Manifold/Algebra/SMul.lean

added theorem ContMDiff.smul

added theorem ContMDiffOn.smul

added theorem ContMDiffSMul.continuousSMul

added theorem ContMDiffWithinAt.smul

added theorem IsScalarTower.contMDiffSMul

added theorem MulAction.contMDiffSMul_compHom

Modified Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean

deleted theorem ContMDiff.smul

deleted theorem ContMDiffOn.smul

deleted theorem ContMDiffWithinAt.smul

deleted theorem contMDiff_smul

Modified Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

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