Structures · Geometry

ContMDiffSMul

Basic typeclass stating that the action of G on M is Cⁿ as a function G × M → M. Unlike with ContMDiffMul (the class stating that multiplication G × G → G within a single type G is Cⁿ), we do not extend IsManifold because ContMDiffSMul contains more explicit arguments than IsManifold and so ContMDiffSMul.toIsManifold could not be an instance anyway: this means that in order for ContMDiffSMul to be meaningful, smoothness of G and M have to be required separately. For example, to state that G is a Cⁿ Lie group with a Cⁿ action on a Cⁿ manifold M, one can use the typeclasses [LieGroup I n G] [IsManifold I' n M] [ContMDiffSMul I I' n G M].

Defined in

Mathlib.Geometry.Manifold.Algebra.SMul

Shape

5 explicit arguments · adds contMDiff_smul