Structures · Geometry

ContMDiffVAdd

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

Defined in

Mathlib.Geometry.Manifold.Algebra.SMul

Shape

5 explicit arguments · adds contMDiff_vadd