LieGroup

📁 Source: Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Statistics

Metric	Count
Definitions `ContMDiffInv₀`, `LieAddGroup`, `LieGroup`	3
Theorems `div`, `div₀`, `inv`, `inv₀`, `neg`, `sub`, `div`, `div₀`, `inv`, `inv₀`, `neg`, `sub`, `contMDiffAt_inv₀`, `of_le`, `div`, `div₀`, `inv`, `inv₀`, `neg`, `sub`, `div`, `div₀`, `inv`, `inv₀`, `neg`, `sub`, `contMDiff_neg`, `of_le`, `toContMDiffAdd`, `contMDiff_inv`, `of_le`, `toContMDiffMul`, `instLieAddGroup`, `instLieGroup`, `contMDiffAt_inv₀`, `contMDiffOn_inv₀`, `contMDiff_inv`, `contMDiff_neg`, `continuousInv₀_of_contMDiffInv₀`, `hasContinuousInv₀_of_hasContMDiffInv₀`, `instContMDiffInv₀ModelWithCornersSelf`, `instContMDiffInv₀OfNatWithTopENat`, `instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀`, `instContMDiffInv₀OfSomeENatTopOfLEInfty`, `instContMDiffInv₀OfTopWithTopENat`, `instLieAddGroupOfNatWithTopENat`, `instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup`, `instLieAddGroupOfSomeENatTopOfLEInfty`, `instLieAddGroupOfTopWithTopENat`, `instLieGroupOfNatWithTopENat`, `instLieGroupOfNatWithTopENatOfIsTopologicalGroup`, `instLieGroupOfSomeENatTopOfLEInfty`, `instLieGroupOfTopWithTopENat`, `instNormedSpaceLieAddGroup`, `topologicalAddGroup_of_lieAddGroup`, `topologicalGroup_of_lieGroup`	56
Total	59

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`ContMDiff`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `LieGroup.toContMDiffMul` `inv`
`div₀` 📖	mathematical	`ContMDiff`	`Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `inv₀`
`inv` 📖	mathematical	`ContMDiff`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ContMDiffAt.inv`
`inv₀` 📖	—	`ContMDiff`	—	—	`ContMDiffAt.inv₀`
`neg` 📖	mathematical	`ContMDiff`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ContMDiffAt.neg`
`sub` 📖	mathematical	`ContMDiff`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `add` `LieAddGroup.toContMDiffAdd` `neg`

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`ContMDiffAt`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `LieGroup.toContMDiffMul` `inv`
`div₀` 📖	mathematical	`ContMDiffAt`	`Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `inv₀`
`inv` 📖	mathematical	`ContMDiffAt`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`comp` `ContMDiff.contMDiffAt` `contMDiff_inv`
`inv₀` 📖	—	`ContMDiffAt`	—	—	`comp` `contMDiffAt_inv₀`
`neg` 📖	mathematical	`ContMDiffAt`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`comp` `ContMDiff.contMDiffAt` `contMDiff_neg`
`sub` 📖	mathematical	`ContMDiffAt`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `add` `LieAddGroup.toContMDiffAdd` `neg`

ContMDiffInv₀

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffAt_inv₀` 📖	mathematical	—	`ContMDiffAt`	—	—
`of_le` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`ContMDiffInv₀`	—	`ContMDiffAt.of_le` `contMDiffAt_inv₀`

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`ContMDiffOn`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `LieGroup.toContMDiffMul` `inv`
`div₀` 📖	mathematical	`ContMDiffOn`	`Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `inv₀`
`inv` 📖	mathematical	`ContMDiffOn`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`ContMDiffWithinAt.inv`
`inv₀` 📖	—	`ContMDiffOn`	—	—	`ContMDiffWithinAt.inv₀`
`neg` 📖	mathematical	`ContMDiffOn`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ContMDiffWithinAt.neg`
`sub` 📖	mathematical	`ContMDiffOn`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `add` `LieAddGroup.toContMDiffAdd` `neg`

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div` 📖	mathematical	`ContMDiffWithinAt`	`DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `LieGroup.toContMDiffMul` `inv`
`div₀` 📖	mathematical	`ContMDiffWithinAt`	`Pi.instDiv` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv` `mul` `inv₀`
`inv` 📖	mathematical	`ContMDiffWithinAt`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`comp` `ContMDiffAt.contMDiffWithinAt` `ContMDiff.contMDiffAt` `contMDiff_inv` `Set.mapsTo_univ`
`inv₀` 📖	—	`ContMDiffWithinAt`	—	—	`ContMDiffAt.comp_contMDiffWithinAt` `contMDiffAt_inv₀`
`neg` 📖	mathematical	`ContMDiffWithinAt`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`comp` `ContMDiffAt.contMDiffWithinAt` `ContMDiff.contMDiffAt` `contMDiff_neg` `Set.mapsTo_univ`
`sub` 📖	mathematical	`ContMDiffWithinAt`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `add` `LieAddGroup.toContMDiffAdd` `neg`

LieAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiff_neg` 📖	mathematical	—	`ContMDiff` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`of_le` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`LieAddGroup`	—	`ContMDiffAdd.of_le` `toContMDiffAdd` `ContMDiff.of_le` `contMDiff_neg`
`toContMDiffAdd` 📖	mathematical	—	`ContMDiffAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—

LieGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiff_inv` 📖	mathematical	—	`ContMDiff` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`of_le` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`LieGroup`	—	`ContMDiffMul.of_le` `toContMDiffMul` `ContMDiff.of_le` `contMDiff_inv`
`toContMDiffMul` 📖	mathematical	—	`ContMDiffMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLieAddGroup` 📖	mathematical	—	`LieAddGroup` `ModelProd` `instTopologicalSpaceModelProd` `normedAddCommGroup` `normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelWithCorners.prod` `instAddGroup` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffAdd.prod` `LieAddGroup.toContMDiffAdd` `ContMDiff.prodMk` `ContMDiff.neg` `contMDiff_fst` `contMDiff_snd`
`instLieGroup` 📖	mathematical	—	`LieGroup` `ModelProd` `instTopologicalSpaceModelProd` `normedAddCommGroup` `normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelWithCorners.prod` `instGroup` `instTopologicalSpaceProd` `prodChartedSpace`	—	`ContMDiffMul.prod` `LieGroup.toContMDiffMul` `ContMDiff.prodMk` `ContMDiff.inv` `contMDiff_fst` `contMDiff_snd`

(root)

Definitions

Name	Category	Theorems
`ContMDiffInv₀` 📖	CompData	6 math math: `instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀`, `instContMDiffInv₀OfSomeENatTopOfLEInfty`, `instContMDiffInv₀OfNatWithTopENat`, `instContMDiffInv₀ModelWithCornersSelf`, `ContMDiffInv₀.of_le`, `instContMDiffInv₀OfTopWithTopENat`
`LieAddGroup` 📖	CompData	8 math math: `instLieAddGroupOfNatWithTopENat`, `instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup`, `instNormedSpaceLieAddGroup`, `instLieAddGroupOfTopWithTopENat`, `LieAddGroup.of_le`, `ContMDiffRing.toLieAddGroup`, `instLieAddGroupOfSomeENatTopOfLEInfty`, `Prod.instLieAddGroup`
`LieGroup` 📖	CompData	8 math math: `Prod.instLieGroup`, `instLieGroupOfNatWithTopENatOfIsTopologicalGroup`, `instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle`, `Units.instLieGroupModelWithCornersSelf`, `instLieGroupOfSomeENatTopOfLEInfty`, `instLieGroupOfTopWithTopENat`, `instLieGroupOfNatWithTopENat`, `LieGroup.of_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffAt_inv₀` 📖	mathematical	—	`ContMDiffAt`	—	`ContMDiffInv₀.contMDiffAt_inv₀`
`contMDiffOn_inv₀` 📖	mathematical	—	`ContMDiffOn` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`ContMDiffAt.contMDiffWithinAt` `contMDiffAt_inv₀`
`contMDiff_inv` 📖	mathematical	—	`ContMDiff` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`LieGroup.contMDiff_inv`
`contMDiff_neg` 📖	mathematical	—	`ContMDiff` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`LieAddGroup.contMDiff_neg`
`continuousInv₀_of_contMDiffInv₀` 📖	mathematical	—	`ContinuousInv₀`	—	`ContMDiffAt.continuousAt` `contMDiffAt_inv₀`
`hasContinuousInv₀_of_hasContMDiffInv₀` 📖	mathematical	—	`ContinuousInv₀`	—	`continuousInv₀_of_contMDiffInv₀`
`instContMDiffInv₀ModelWithCornersSelf` 📖	mathematical	—	`ContMDiffInv₀` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `modelWithCornersSelf` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `NormedField.toField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `chartedSpaceSelf`	—	`contMDiffAt_iff_contDiffAt` `contDiffAt_inv`
`instContMDiffInv₀OfNatWithTopENat` 📖	mathematical	—	`ContMDiffInv₀` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.instAtLeastTwoHAddOfNat` `ContMDiffInv₀.of_le` `one_le_two` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid`
`instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀` 📖	mathematical	—	`ContMDiffInv₀` `WithTop` `ENat` `WithTop.zero` `instZeroENat`	—	`ModelWithCorners.t1Space` `contMDiffOn_zero_iff` `continuousOn_inv₀` `ContMDiffWithinAt.contMDiffAt` `IsOpen.mem_nhds` `isOpen_compl_singleton`
`instContMDiffInv₀OfSomeENatTopOfLEInfty` 📖	mathematical	—	`ContMDiffInv₀`	—	`ContMDiffInv₀.of_le` `ENat.LEInfty.out`
`instContMDiffInv₀OfTopWithTopENat` 📖	mathematical	—	`ContMDiffInv₀`	—	`ContMDiffInv₀.of_le` `le_top`
`instLieAddGroupOfNatWithTopENat` 📖	mathematical	—	`LieAddGroup` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.instAtLeastTwoHAddOfNat` `LieAddGroup.of_le` `one_le_two` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid`
`instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup` 📖	mathematical	—	`LieAddGroup` `WithTop` `ENat` `WithTop.zero` `instZeroENat`	—	`instContMDiffAddOfNatWithTopENatOfContinuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `contMDiff_zero_iff` `ContinuousNeg.continuous_neg` `IsTopologicalAddGroup.toContinuousNeg`
`instLieAddGroupOfSomeENatTopOfLEInfty` 📖	mathematical	—	`LieAddGroup`	—	`LieAddGroup.of_le` `ENat.LEInfty.out`
`instLieAddGroupOfTopWithTopENat` 📖	mathematical	—	`LieAddGroup`	—	`LieAddGroup.of_le` `le_top`
`instLieGroupOfNatWithTopENat` 📖	mathematical	—	`LieGroup` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Nat.instAtLeastTwoHAddOfNat` `LieGroup.of_le` `one_le_two` `WithTop.zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid`
`instLieGroupOfNatWithTopENatOfIsTopologicalGroup` 📖	mathematical	—	`LieGroup` `WithTop` `ENat` `WithTop.zero` `instZeroENat`	—	`instContMDiffMulOfNatWithTopENatOfContinuousMul` `IsTopologicalGroup.toContinuousMul` `contMDiff_zero_iff` `ContinuousInv.continuous_inv` `IsTopologicalGroup.toContinuousInv`
`instLieGroupOfSomeENatTopOfLEInfty` 📖	mathematical	—	`LieGroup`	—	`LieGroup.of_le` `ENat.LEInfty.out`
`instLieGroupOfTopWithTopENat` 📖	mathematical	—	`LieGroup`	—	`LieGroup.of_le` `le_top`
`instNormedSpaceLieAddGroup` 📖	mathematical	—	`LieAddGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `chartedSpaceSelf`	—	`instContMDiffAddSelf` `ContDiff.contMDiff` `contDiff_neg`
`topologicalAddGroup_of_lieAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup`	—	`continuousAdd_of_contMDiffAdd` `LieAddGroup.toContMDiffAdd` `ContMDiff.continuous` `contMDiff_neg`
`topologicalGroup_of_lieGroup` 📖	mathematical	—	`IsTopologicalGroup`	—	`continuousMul_of_contMDiffMul` `LieGroup.toContMDiffMul` `ContMDiff.continuous` `contMDiff_inv`

---

← Back to Index