LeftInvariantDerivation

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

Statistics

Metric	Count
Definitions LeftInvariantDerivation, coeFnAddMonoidHom, evalAt, hasIntScalar, hasNatScalar, instAdd, instAddCommGroup, instBracket, instCoeDerivationContMDiffMapModelWithCornersSelfSomeENatTop, instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop, instInhabited, instLieAlgebra, instLieRing, instModule, instNeg, instSMul, instSub, instZero, toDerivation	19
Theorems coeFnAddMonoidHom_apply, coe_add, coe_derivation, coe_injective, coe_neg, coe_smul, coe_sub, coe_zero, commutator_apply, commutator_coe_derivation, comp_L, evalAt_apply, evalAt_coe, evalAt_mul, ext, ext_iff, instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop, left_invariant, left_invariant', left_invariant'', leibniz, lift_add, lift_smul, lift_zero, map_add, map_neg, map_smul, map_sub, map_zero, toDerivation_injective, toFun_eq_coe	31
Total	50

LeftInvariantDerivation

Definitions

Name	Category	Theorems
coeFnAddMonoidHom 📖	CompOp	1 math math: coeFnAddMonoidHom_apply
evalAt 📖	CompOp	4 math math: left_invariant, evalAt_coe, evalAt_mul, evalAt_apply
hasIntScalar 📖	CompOp	—
hasNatScalar 📖	CompOp	—
instAdd 📖	CompOp	2 math math: lift_add, coe_add
instAddCommGroup 📖	CompOp	5 math math: left_invariant, evalAt_coe, evalAt_mul, coeFnAddMonoidHom_apply, evalAt_apply
instBracket 📖	CompOp	2 math math: commutator_apply, commutator_coe_derivation
instCoeDerivationContMDiffMapModelWithCornersSelfSomeENatTop 📖	CompOp	—
instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop 📖	CompOp	21 math math: leibniz, coe_derivation, comp_L, map_zero, coe_sub, map_add, coe_add, coe_injective, coe_neg, map_smul, coe_smul, map_sub, map_neg, coe_zero, commutator_apply, commutator_coe_derivation, ext_iff, toFun_eq_coe, instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop, coeFnAddMonoidHom_apply, evalAt_apply
instInhabited 📖	CompOp	—
instLieAlgebra 📖	CompOp	—
instLieRing 📖	CompOp	—
instModule 📖	CompOp	4 math math: left_invariant, evalAt_coe, evalAt_mul, evalAt_apply
instNeg 📖	CompOp	1 math math: coe_neg
instSMul 📖	CompOp	2 math math: lift_smul, coe_smul
instSub 📖	CompOp	1 math math: coe_sub
instZero 📖	CompOp	2 math math: lift_zero, coe_zero
toDerivation 📖	CompOp	10 math math: lift_zero, coe_derivation, left_invariant', lift_add, lift_smul, evalAt_coe, left_invariant'', toDerivation_injective, commutator_coe_derivation, toFun_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom LeftInvariantDerivation AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat ContMDiffMap.addMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf AddMonoidHom.instFunLike coeFnAddMonoidHom instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	instContMDiffAddSelf
coe_add 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop instAdd Pi.instAdd ContMDiffMap.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing instContMDiffAddSelf	—	—
coe_derivation 📖	mathematical	—	DFunLike.coe Derivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring Field.toSemifield NormedField.toField CommRing.toCommSemiring ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module Derivation.instFunLike toDerivation LeftInvariantDerivation instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	instFieldContMDiffRing instContMDiffAddSelf
coe_injective 📖	mathematical	—	LeftInvariantDerivation DFunLike.coe ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	DFunLike.coe_injective
coe_neg 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffMap.addCommGroup NormedAddCommGroup.toAddCommGroup instNormedSpaceLieAddGroup	—	—
coe_smul 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop instSMul Function.hasSMul ContMDiffMap.instSMul	—	—
coe_sub 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid ContMDiffMap.addGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup instNormedSpaceLieAddGroup	—	—
coe_zero 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop instZero Pi.instZero ContMDiffMap.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	—
commutator_apply 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop Bracket.bracket instBracket SubNegMonoid.toSub AddGroup.toSubNegMonoid ContMDiffMap.addGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup instNormedSpaceLieAddGroup	—	—
commutator_coe_derivation 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop Bracket.bracket instBracket Derivation Semifield.toCommSemiring Field.toSemifield NormedField.toField CommRing.toCommSemiring ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module Derivation.instFunLike Derivation.instBracket toDerivation	—	—
comp_L 📖	mathematical	—	ContMDiffMap.comp NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat DFunLike.coe LeftInvariantDerivation ContMDiffMap instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop smoothLeftMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	ContMDiffMap.ext ContMDiffMap.comp_apply L_apply Algebra.to_smulCommClass IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop evalAt_apply evalAt_mul hfdifferential_apply fdifferential_apply
evalAt_apply 📖	mathematical	—	DFunLike.coe PointDerivation PointedContMDiffMap WithTop.some ENat Top.top instTopENat Derivation.instFunLike Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField CommRing.toCommSemiring PointedContMDiffMap.instCommRingSomeENatTop ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PointedContMDiffMap.instAlgebraSomeENatTop Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring PointedContMDiffMap.evalAlgebra NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap RingHom.id Semiring.toNonAssocSemiring LeftInvariantDerivation AddCommGroup.toAddCommMonoid instAddCommGroup Derivation.instAddCommMonoid instModule Derivation.instModule Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.to_smulCommClass LieAlgebra.toModule LieRing.ofAssociativeRing NormedRing.toRing NormedCommRing.toNormedRing LieAlgebra.ofAssociativeAlgebra PointedContMDiffMap.instIsScalarTowerSomeENatTop LinearMap.instFunLike evalAt ContMDiffMap SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf ContMDiffMap.instFunLike instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop
evalAt_coe 📖	mathematical	—	DFunLike.coe LinearMap PointedContMDiffMap WithTop.some ENat Top.top instTopENat CommSemiring.toSemiring CommRing.toCommSemiring PointedContMDiffMap.instCommRingSomeENatTop RingHom.id Semiring.toNonAssocSemiring Derivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf Semifield.toCommSemiring Field.toSemifield NormedField.toField ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module PointDerivation Derivation.instAddCommMonoid PointedContMDiffMap.instAlgebraSomeENatTop Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring PointedContMDiffMap.evalAlgebra NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Derivation.instModule ContMDiffMap.semiring PointedContMDiffMap.instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf Algebra.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike Derivation.evalAt toDerivation LeftInvariantDerivation AddCommGroup.toAddCommMonoid instAddCommGroup instModule Algebra.id LieAlgebra.toModule LieRing.ofAssociativeRing NormedRing.toRing NormedCommRing.toNormedRing LieAlgebra.ofAssociativeAlgebra evalAt	—	instFieldContMDiffRing instContMDiffAddSelf IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf Algebra.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop smulCommClass_self
evalAt_mul 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring LeftInvariantDerivation PointDerivation MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AddCommGroup.toAddCommMonoid instAddCommGroup Derivation.instAddCommMonoid PointedContMDiffMap WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring CommRing.toCommSemiring PointedContMDiffMap.instCommRingSomeENatTop ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PointedContMDiffMap.instAlgebraSomeENatTop Algebra.toModule PointedContMDiffMap.evalAlgebra NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace instModule Derivation.instModule Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.to_smulCommClass LieAlgebra.toModule LieRing.ofAssociativeRing NormedRing.toRing NormedCommRing.toNormedRing LieAlgebra.ofAssociativeAlgebra PointedContMDiffMap.instIsScalarTowerSomeENatTop LinearMap.instFunLike evalAt hfdifferential smoothLeftMul L_apply	—	Derivation.ext Algebra.to_smulCommClass IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop L_apply smoothLeftMul_one left_invariant hfdifferential_apply L_mul RingHomCompTriple.ids fdifferential_comp fdifferential_apply
ext 📖	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	ext
instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop 📖	mathematical	—	LinearMapClass LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf ContMDiffMap.module instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	instContMDiffAddSelf map_add instFieldContMDiffRing AddMonoidHomClass.toAddHomClass Derivation.instAddMonoidHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
left_invariant 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring PointDerivation MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Derivation.instAddCommMonoid PointedContMDiffMap WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring CommRing.toCommSemiring PointedContMDiffMap.instCommRingSomeENatTop ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PointedContMDiffMap.instAlgebraSomeENatTop Algebra.toModule PointedContMDiffMap.evalAlgebra NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Derivation.instModule Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop LinearMap.instFunLike hfdifferential smoothLeftMul MulOne.toMul smoothLeftMul_one LeftInvariantDerivation AddCommGroup.toAddCommMonoid instAddCommGroup instModule LieAlgebra.toModule LieRing.ofAssociativeRing NormedRing.toRing NormedCommRing.toNormedRing LieAlgebra.ofAssociativeAlgebra evalAt	—	left_invariant''
left_invariant' 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring PointDerivation MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Derivation.instAddCommMonoid PointedContMDiffMap WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring CommRing.toCommSemiring PointedContMDiffMap.instCommRingSomeENatTop ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PointedContMDiffMap.instAlgebraSomeENatTop Algebra.toModule PointedContMDiffMap.evalAlgebra NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Derivation.instModule Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop LinearMap.instFunLike hfdifferential smoothLeftMul MulOne.toMul smoothLeftMul_one Derivation ContMDiffMap SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module ContMDiffMap.semiring PointedContMDiffMap.instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.evalAt toDerivation	—	left_invariant''
left_invariant'' 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring PointDerivation MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Derivation.instAddCommMonoid PointedContMDiffMap WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring CommRing.toCommSemiring PointedContMDiffMap.instCommRingSomeENatTop ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing PointedContMDiffMap.instAlgebraSomeENatTop Algebra.toModule PointedContMDiffMap.evalAlgebra NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace Derivation.instModule Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop LinearMap.instFunLike hfdifferential smoothLeftMul MulOne.toMul smoothLeftMul_one Derivation ContMDiffMap SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module ContMDiffMap.semiring PointedContMDiffMap.instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.evalAt toDerivation	—	—
leibniz 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop ContMDiffMap.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing instContMDiffMulOfTopWithTopENat WithTop WithTop.top ContMDiffRing.toContMDiffMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instFieldContMDiffRing ContMDiffMap.instAdd Distrib.toAdd instContMDiffAddSelf ContMDiffMap.instSMul'	—	Derivation.leibniz' instFieldContMDiffRing instContMDiffAddSelf
lift_add 📖	mathematical	—	toDerivation LeftInvariantDerivation instAdd Derivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring Field.toSemifield NormedField.toField CommRing.toCommSemiring ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module Derivation.instAdd	—	instFieldContMDiffRing instContMDiffAddSelf
lift_smul 📖	mathematical	—	toDerivation LeftInvariantDerivation instSMul Derivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring Field.toSemifield NormedField.toField CommRing.toCommSemiring ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module Derivation.instSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Algebra.to_smulCommClass ContMDiffMap.semiring	—	instFieldContMDiffRing instContMDiffAddSelf
lift_zero 📖	mathematical	—	toDerivation LeftInvariantDerivation instZero Derivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring Field.toSemifield NormedField.toField CommRing.toCommSemiring ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module Derivation.instZero	—	instFieldContMDiffRing instContMDiffAddSelf
map_add 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop ContMDiffMap.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing instContMDiffAddSelf	—	instContMDiffAddSelf map_add SemilinearMapClass.toAddHomClass instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop
map_neg 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffMap.addCommGroup NormedAddCommGroup.toAddCommGroup instNormedSpaceLieAddGroup	—	instNormedSpaceLieAddGroup map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass instContMDiffAddSelf SemilinearMapClass.distribMulActionSemiHomClass instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop
map_smul 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop ContMDiffMap.instSMul	—	map_smul SemilinearMapClass.toMulActionSemiHomClass instContMDiffAddSelf instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop
map_sub 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop SubNegMonoid.toSub AddGroup.toSubNegMonoid ContMDiffMap.addGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup instNormedSpaceLieAddGroup	—	instNormedSpaceLieAddGroup map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass instContMDiffAddSelf SemilinearMapClass.distribMulActionSemiHomClass instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop
map_zero 📖	mathematical	—	DFunLike.coe LeftInvariantDerivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop ContMDiffMap.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	map_zero AddMonoidHomClass.toZeroHomClass instContMDiffAddSelf DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop
toDerivation_injective 📖	mathematical	—	LeftInvariantDerivation Derivation ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat Semifield.toCommSemiring Field.toSemifield NormedField.toField CommRing.toCommSemiring ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module toDerivation	—	instFieldContMDiffRing instContMDiffAddSelf Algebra.to_smulCommClass IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop smoothLeftMul_one PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf smulCommClass_self
toFun_eq_coe 📖	mathematical	—	AddHom.toFun ContMDiffMap NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing chartedSpaceSelf WithTop.some ENat Top.top instTopENat AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instFieldContMDiffRing ContMDiffMap.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instContMDiffAddSelf LinearMap.toAddHom Semifield.toCommSemiring Field.toSemifield RingHom.id Algebra.toModule smoothFunctionsAlgebra ContMDiffMap.module Derivation.toLinearMap ContMDiffMap.module' toDerivation DFunLike.coe LeftInvariantDerivation instFunLikeContMDiffMapModelWithCornersSelfSomeENatTop	—	instFieldContMDiffRing instContMDiffAddSelf

(root)

Definitions

Name	Category	Theorems
LeftInvariantDerivation 📖	CompData	28 math math: LeftInvariantDerivation.lift_zero, LeftInvariantDerivation.leibniz, LeftInvariantDerivation.coe_derivation, LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.lift_add, LeftInvariantDerivation.lift_smul, LeftInvariantDerivation.comp_L, LeftInvariantDerivation.evalAt_coe, LeftInvariantDerivation.map_zero, LeftInvariantDerivation.coe_sub, LeftInvariantDerivation.map_add, LeftInvariantDerivation.coe_add, LeftInvariantDerivation.coe_injective, LeftInvariantDerivation.coe_neg, LeftInvariantDerivation.map_smul, LeftInvariantDerivation.coe_smul, LeftInvariantDerivation.map_sub, LeftInvariantDerivation.map_neg, LeftInvariantDerivation.coe_zero, LeftInvariantDerivation.toDerivation_injective, LeftInvariantDerivation.evalAt_mul, LeftInvariantDerivation.commutator_apply, LeftInvariantDerivation.commutator_coe_derivation, LeftInvariantDerivation.ext_iff, LeftInvariantDerivation.toFun_eq_coe, LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop, LeftInvariantDerivation.coeFnAddMonoidHom_apply, LeftInvariantDerivation.evalAt_apply

---

← Back to Index