GroupLieAlgebra

📁 Source: Mathlib/Geometry/Manifold/GroupLieAlgebra.lean

Statistics

Metric	Count
Definitions AddGroupLieAlgebra, GroupLieAlgebra, addInvariantVectorField, instBracketAddGroupLieAlgebra, instBracketGroupLieAlgebra, instLieAlgebraAddGroupLieAlgebra, instLieAlgebraGroupLieAlgebra, instLieRingAddGroupLieAlgebra, instLieRingGroupLieAlgebra, mulInvariantVectorField	10
Theorems bracket_def, bracket_def, addInvariantVectorField_add, addInvariantVectorField_eq_mpullback, addInvariantVectorField_smul, addInvariantVector_mlieBracket, contMDiffAt_addInvariantVectorField, contMDiffAt_mulInvariantVectorField, contMDiff_addInvariantVectorField, contMDiff_mulInvariantVectorField, inverse_mfderiv_add_left, inverse_mfderiv_mul_left, mdifferentiableAt_addInvariantVectorField, mdifferentiableAt_mulInvariantVectorField, mdifferentiable_addInvariantVectorField, mdifferentiable_mulInvariantVectorField, mpullback_addInvariantVectorField, mpullback_mulInvariantVectorField, mulInvariantVectorField_add, mulInvariantVectorField_eq_mpullback, mulInvariantVectorField_smul, mulInvariantVector_mlieBracket	22
Total	32

AddGroupLieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bracket_def 📖	mathematical	—	Bracket.bracket AddGroupLieAlgebra instBracketAddGroupLieAlgebra VectorField.mlieBracket addInvariantVectorField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—

GroupLieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bracket_def 📖	mathematical	—	Bracket.bracket GroupLieAlgebra instBracketGroupLieAlgebra VectorField.mlieBracket mulInvariantVectorField InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—

(root)

Definitions

Name	Category	Theorems
AddGroupLieAlgebra 📖	CompOp	3 math math: AddGroupLieAlgebra.bracket_def, addInvariantVectorField_smul, addInvariantVectorField_add
GroupLieAlgebra 📖	CompOp	3 math math: mulInvariantVectorField_smul, GroupLieAlgebra.bracket_def, mulInvariantVectorField_add
addInvariantVectorField 📖	CompOp	10 math math: AddGroupLieAlgebra.bracket_def, contMDiff_addInvariantVectorField, addInvariantVectorField_smul, mdifferentiableAt_addInvariantVectorField, addInvariantVectorField_eq_mpullback, mpullback_addInvariantVectorField, mdifferentiable_addInvariantVectorField, addInvariantVector_mlieBracket, contMDiffAt_addInvariantVectorField, addInvariantVectorField_add
instBracketAddGroupLieAlgebra 📖	CompOp	1 math math: AddGroupLieAlgebra.bracket_def
instBracketGroupLieAlgebra 📖	CompOp	1 math math: GroupLieAlgebra.bracket_def
instLieAlgebraAddGroupLieAlgebra 📖	CompOp	—
instLieAlgebraGroupLieAlgebra 📖	CompOp	—
instLieRingAddGroupLieAlgebra 📖	CompOp	—
instLieRingGroupLieAlgebra 📖	CompOp	—
mulInvariantVectorField 📖	CompOp	10 math math: contMDiff_mulInvariantVectorField, contMDiffAt_mulInvariantVectorField, mulInvariantVector_mlieBracket, mdifferentiable_mulInvariantVectorField, mdifferentiableAt_mulInvariantVectorField, mulInvariantVectorField_smul, GroupLieAlgebra.bracket_def, mpullback_mulInvariantVectorField, mulInvariantVectorField_eq_mpullback, mulInvariantVectorField_add

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addInvariantVectorField_add 📖	mathematical	—	addInvariantVectorField AddGroupLieAlgebra AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.instAdd TangentSpace	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
addInvariantVectorField_eq_mpullback 📖	mathematical	—	addInvariantVectorField NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid VectorField.mpullback AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg	—	Nat.instAtLeastTwoHAddOfNat neg_add_cancel inverse_mfderiv_add_left neg_neg
addInvariantVectorField_smul 📖	mathematical	—	addInvariantVectorField AddGroupLieAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace Pi.instSMul TangentSpace SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
addInvariantVector_mlieBracket 📖	mathematical	—	addInvariantVectorField VectorField.mlieBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Nat.instAtLeastTwoHAddOfNat addInvariantVectorField_eq_mpullback VectorField.mpullback_mlieBracket instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold LieAddGroup.toContMDiffAdd mdifferentiableAt_addInvariantVectorField contMDiffAt_add_left minSmoothness_monotone Nat.cast_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero mpullback_addInvariantVectorField
contMDiffAt_addInvariantVectorField 📖	mathematical	—	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LieAddGroup.toContMDiffAdd FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle addInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat ContMDiff.contMDiffAt instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold LieAddGroup.toContMDiffAdd contMDiff_addInvariantVectorField
contMDiffAt_mulInvariantVectorField 📖	mathematical	—	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LieGroup.toContMDiffMul FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle mulInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat ContMDiff.contMDiffAt instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold LieGroup.toContMDiffMul contMDiff_mulInvariantVectorField
contMDiff_addInvariantVectorField 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LieAddGroup.toContMDiffAdd FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle addInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' lt_of_lt_of_le Nat.ofNat_pos WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness minSmoothness_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold LieAddGroup.toContMDiffAdd Bundle.contMDiff_zeroSection TangentSpace.vectorBundle contMDiff_const ContMDiff.prodMk IsManifold.prod contMDiff_equivTangentBundleProd_symm ContMDiff.contMDiff_tangentMap contMDiff_add le_rfl ContMDiff.comp add_zero mfderiv_prod_eq_add_apply ContMDiff.mdifferentiableAt map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass zero_add
contMDiff_mulInvariantVectorField 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LieGroup.toContMDiffMul FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle mulInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' lt_of_lt_of_le WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness minSmoothness_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold LieGroup.toContMDiffMul Bundle.contMDiff_zeroSection TangentSpace.vectorBundle contMDiff_const ContMDiff.prodMk IsManifold.prod contMDiff_equivTangentBundleProd_symm ContMDiff.contMDiff_tangentMap contMDiff_mul le_rfl ContMDiff.comp mul_one mfderiv_prod_eq_add_apply ContMDiff.mdifferentiableAt map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass zero_add
inverse_mfderiv_add_left 📖	mathematical	—	ContinuousLinearMap.inverse TangentSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instTopologicalSpaceTangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace mfderiv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' lt_of_lt_of_le Nat.ofNat_pos WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness neg_add_cancel_left mfderiv_id add_neg_cancel_left ContinuousLinearMap.inverse_eq RingHomCompTriple.ids mfderiv_comp ContMDiffAt.mdifferentiableAt ContMDiff.contMDiffAt contMDiff_add_left LieAddGroup.toContMDiffAdd
inverse_mfderiv_mul_left 📖	mathematical	—	ContinuousLinearMap.inverse TangentSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instTopologicalSpaceTangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace mfderiv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' lt_of_lt_of_le WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness inv_mul_cancel_left mfderiv_id mul_inv_cancel_left ContinuousLinearMap.inverse_eq RingHomCompTriple.ids mfderiv_comp ContMDiffAt.mdifferentiableAt ContMDiff.contMDiffAt contMDiff_mul_left LieGroup.toContMDiffMul
mdifferentiableAt_addInvariantVectorField 📖	mathematical	—	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LieAddGroup.toContMDiffAdd FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle addInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat ContMDiffAt.mdifferentiableAt instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold LieAddGroup.toContMDiffAdd contMDiffAt_addInvariantVectorField LT.lt.ne' lt_of_lt_of_le Nat.ofNat_pos WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness
mdifferentiableAt_mulInvariantVectorField 📖	mathematical	—	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LieGroup.toContMDiffMul FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle mulInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat ContMDiffAt.mdifferentiableAt instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold LieGroup.toContMDiffMul contMDiffAt_mulInvariantVectorField LT.lt.ne' lt_of_lt_of_le WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness
mdifferentiable_addInvariantVectorField 📖	mathematical	—	MDifferentiable Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid LieAddGroup.toContMDiffAdd FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle addInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat ContMDiff.mdifferentiable instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffAdd.toIsManifold LieAddGroup.toContMDiffAdd contMDiff_addInvariantVectorField LT.lt.ne' lt_of_lt_of_le Nat.ofNat_pos WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness
mdifferentiable_mulInvariantVectorField 📖	mathematical	—	MDifferentiable Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LieGroup.toContMDiffMul FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle mulInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat ContMDiff.mdifferentiable instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold LieGroup.toContMDiffMul contMDiff_mulInvariantVectorField LT.lt.ne' lt_of_lt_of_le WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness
mpullback_addInvariantVectorField 📖	mathematical	—	VectorField.mpullback AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid addInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' lt_of_lt_of_le Nat.ofNat_pos WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness inverse_mfderiv_add_left neg_one_zsmul add_assoc add_one_zsmul neg_add_cancel zero_zsmul zero_add RingHomCompTriple.ids mfderiv_comp ContMDiffAt.mdifferentiableAt ContMDiff.contMDiffAt contMDiff_add_left LieAddGroup.toContMDiffAdd add_zero
mpullback_mulInvariantVectorField 📖	mathematical	—	VectorField.mpullback MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid mulInvariantVectorField	—	Nat.instAtLeastTwoHAddOfNat LT.lt.ne' lt_of_lt_of_le WithTop.instIsOrderedRing WithTop.nontrivial le_minSmoothness inverse_mfderiv_mul_left neg_add_cancel zpow_zero one_mul RingHomCompTriple.ids mfderiv_comp ContMDiffAt.mdifferentiableAt ContMDiff.contMDiffAt contMDiff_mul_left LieGroup.toContMDiffMul mul_one
mulInvariantVectorField_add 📖	mathematical	—	mulInvariantVectorField GroupLieAlgebra AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.instAdd TangentSpace	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
mulInvariantVectorField_eq_mpullback 📖	mathematical	—	mulInvariantVectorField InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid VectorField.mpullback MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv	—	Nat.instAtLeastTwoHAddOfNat inv_mul_cancel inverse_mfderiv_mul_left inv_inv
mulInvariantVectorField_smul 📖	mathematical	—	mulInvariantVectorField GroupLieAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace Pi.instSMul TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
mulInvariantVector_mlieBracket 📖	mathematical	—	mulInvariantVectorField VectorField.mlieBracket InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Nat.instAtLeastTwoHAddOfNat mulInvariantVectorField_eq_mpullback VectorField.mpullback_mlieBracket instIsManifoldMinSmoothnessOfNatWithTopENat ContMDiffMul.toIsManifold LieGroup.toContMDiffMul mdifferentiableAt_mulInvariantVectorField contMDiffAt_mul_left minSmoothness_monotone WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero mpullback_mulInvariantVectorField

---

← Back to Index