DerivationBundle

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

Statistics

Metric	Count
Definitions evalAt, evalAt, «termC^_⟮_,_;_⟯⟨_⟩», «term𝒅», «term𝒅ₕ», PointDerivation, PointedContMDiffMap, eval, evalAlgebra, instAlgebraSomeENatTop, instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf, instCommRingSomeENatTop, instFunLike, instInhabitedSomeENatTop, fdifferential, hfdifferential, smoothFunctionsAlgebra	17
Theorems evalAt_apply, instIsScalarTowerSomeENatTop, instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, smul_def, fdifferential_apply, fdifferential_comp, hfdifferential_apply, smooth_functions_tower	8
Total	25

ContMDiffFunction

Definitions

Name	Category	Theorems
evalAt 📖	CompOp	—

Derivation

Definitions

Name	Category	Theorems
evalAt 📖	CompOp	4 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.evalAt_coe, LeftInvariantDerivation.left_invariant'', evalAt_apply
«termC^_⟮_,_;_⟯⟨_⟩» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalAt_apply 📖	mathematical	—	DFunLike.coe PointDerivation PointedContMDiffMap WithTop.some ENat Top.top instTopENat 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 CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Derivation ContMDiffMap SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf ContMDiffMap.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldContMDiffRing ContMDiffMap.addCommMonoid instContMDiffAddSelf smoothFunctionsAlgebra ContMDiffMap.module' ContMDiffMap.module instAddCommMonoid 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 evalAt ContMDiffMap.instFunLike	—	instFieldContMDiffRing instContMDiffAddSelf IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf Algebra.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop smulCommClass_self

Manifold

Definitions

Name	Category	Theorems
«term𝒅» 📖	CompOp	—
«term𝒅ₕ» 📖	CompOp	—

PointedContMDiffMap

Definitions

Name	Category	Theorems
eval 📖	CompOp	—
evalAlgebra 📖	CompOp	12 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.evalAt_coe, smul_def, fdifferential_apply, LeftInvariantDerivation.left_invariant'', instIsScalarTowerSomeENatTop, fdifferential_comp, hfdifferential_apply, LeftInvariantDerivation.evalAt_mul, Derivation.evalAt_apply, LeftInvariantDerivation.evalAt_apply
instAlgebraSomeENatTop 📖	CompOp	12 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.evalAt_coe, fdifferential_apply, LeftInvariantDerivation.left_invariant'', instIsScalarTowerSomeENatTop, fdifferential_comp, instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, hfdifferential_apply, LeftInvariantDerivation.evalAt_mul, Derivation.evalAt_apply, LeftInvariantDerivation.evalAt_apply
instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf 📖	CompOp	5 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.evalAt_coe, LeftInvariantDerivation.left_invariant'', instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, Derivation.evalAt_apply
instCommRingSomeENatTop 📖	CompOp	13 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.evalAt_coe, smul_def, fdifferential_apply, LeftInvariantDerivation.left_invariant'', instIsScalarTowerSomeENatTop, fdifferential_comp, instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, hfdifferential_apply, LeftInvariantDerivation.evalAt_mul, Derivation.evalAt_apply, LeftInvariantDerivation.evalAt_apply
instFunLike 📖	CompOp	1 math math: smul_def
instInhabitedSomeENatTop 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsScalarTowerSomeENatTop 📖	mathematical	—	IsScalarTower PointedContMDiffMap WithTop.some ENat Top.top instTopENat Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField CommSemiring.toSemiring CommRing.toCommSemiring instCommRingSomeENatTop instAlgebraSomeENatTop DivisionSemiring.toSemiring Semifield.toDivisionSemiring evalAlgebra Algebra.id	—	smul_def ContMDiffMap.coe_smul Pi.smul_apply smul_eq_mul mul_assoc
instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf 📖	mathematical	—	IsScalarTower PointedContMDiffMap WithTop.some ENat Top.top instTopENat 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 Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField CommSemiring.toSemiring CommRing.toCommSemiring instCommRingSomeENatTop instAlgebraSomeENatTop ContMDiffMap.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring instFieldContMDiffRing instAlgebraSomeENatTopContMDiffMapModelWithCornersSelf ContMDiffMap.instSMul	—	IsScalarTower.right
smul_def 📖	mathematical	—	PointedContMDiffMap WithTop.some ENat Top.top instTopENat Algebra.toSMul CommRing.toCommSemiring instCommRingSomeENatTop DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField evalAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DFunLike.coe instFunLike	—	—

(root)

Definitions

Name	Category	Theorems
PointDerivation 📖	CompOp	10 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.evalAt_coe, fdifferential_apply, LeftInvariantDerivation.left_invariant'', fdifferential_comp, hfdifferential_apply, LeftInvariantDerivation.evalAt_mul, Derivation.evalAt_apply, LeftInvariantDerivation.evalAt_apply
PointedContMDiffMap 📖	CompOp	13 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.evalAt_coe, PointedContMDiffMap.smul_def, fdifferential_apply, LeftInvariantDerivation.left_invariant'', PointedContMDiffMap.instIsScalarTowerSomeENatTop, fdifferential_comp, PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, hfdifferential_apply, LeftInvariantDerivation.evalAt_mul, Derivation.evalAt_apply, LeftInvariantDerivation.evalAt_apply
fdifferential 📖	CompOp	3 math math: fdifferential_apply, fdifferential_comp, hfdifferential_apply
hfdifferential 📖	CompOp	5 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.left_invariant'', hfdifferential_apply, LeftInvariantDerivation.evalAt_mul
smoothFunctionsAlgebra 📖	CompOp	11 math math: LeftInvariantDerivation.lift_zero, LeftInvariantDerivation.coe_derivation, LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.lift_add, LeftInvariantDerivation.lift_smul, LeftInvariantDerivation.evalAt_coe, LeftInvariantDerivation.left_invariant'', LeftInvariantDerivation.toDerivation_injective, LeftInvariantDerivation.commutator_coe_derivation, LeftInvariantDerivation.toFun_eq_coe, Derivation.evalAt_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fdifferential_apply 📖	mathematical	—	DFunLike.coe PointDerivation ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike PointedContMDiffMap 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 Derivation.instAddCommMonoid Derivation.instModule Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop LinearMap.instFunLike fdifferential ContMDiffMap.comp SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop
fdifferential_comp 📖	mathematical	—	fdifferential ContMDiffMap.comp WithTop.some ENat Top.top instTopENat LinearMap.comp PointDerivation DFunLike.coe ContMDiffMap ContMDiffMap.instFunLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Derivation.instAddCommMonoid PointedContMDiffMap 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 RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop
hfdifferential_apply 📖	mathematical	DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike	PointDerivation PointedContMDiffMap 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 Derivation.instAddCommMonoid Derivation.instModule Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop LinearMap.instFunLike hfdifferential fdifferential	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass PointedContMDiffMap.instIsScalarTowerSomeENatTop
smooth_functions_tower 📖	mathematical	—	IsScalarTower 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.instSMul ContMDiffMap.instSMul'	—	IsScalarTower.right instFieldContMDiffRing

---

← Back to Index