Structures · Geometry
LieGroup
A (multiplicative) Lie group is a group and a C^n manifold at the same time in which
the multiplication and inverse operations are C^n.
- Shape
- 3 explicit arguments · adds contMDiff_inv
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Real
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- ContMDiffWithinAt.inv
- LieGroup.contMDiff_inv
- contMDiff_mulInvariantVectorField
- inverse_mfderiv_mul_left
- ContMDiffAt.inv
- contMDiff_inv
- mdifferentiableAt_mulInvariantVectorField
- contMDiffAt_mulInvariantVectorField
- ContMDiff.inv
- ContMDiffOn.inv
- mpullback_mulInvariantVectorField
- mulInvariantVectorField_eq_mpullback
- Prod.instLieGroup
- smoothSheafCommGroup
- instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf
- instLieRingGroupLieAlgebra
- ContMDiffOn.div
- LieGroup.toContMDiffMul
- ContMDiffWithinAt.div
- ContMDiffAt.div
- smoothSheafCommGroup.compLeft
- ContMDiffMap.coe_div
- mdifferentiable_mulInvariantVectorField
- smoothPresheafCommGroup
- mulInvariantVector_mlieBracket
- ContMDiffMap.group
- topologicalGroup_of_lieGroup
- smoothPresheafGroup
- ContMDiff.div
- ContMDiffMap.commGroup
- instLieGroupOfNatWithTopENat
- instLieGroupOfTopWithTopENat
- instLieGroupOfSomeENatTopOfLEInfty
- instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf
- smoothSheafGroup
- LieGroup.of_le
- instLieAlgebraGroupLieAlgebra
- ContMDiffMap.coe_inv