SmoothFunctions

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

Statistics

Metric	Count
Definitions `C`, `addCommGroup`, `addCommMonoid`, `addGroup`, `addMonoid`, `addSemigroup`, `algebra`, `coeFnAddMonoidHom`, `coeFnAlgHom`, `coeFnLinearMap`, `coeFnMonoidHom`, `coeFnRingHom`, `commGroup`, `commMonoid`, `commRing`, `compLeftAddMonoidHom`, `compLeftMonoidHom`, `compLeftRingHom`, `evalRingHom`, `group`, `instAdd`, `instMul`, `instNSMul`, `instOne`, `instPow`, `instSMul`, `instSMul'`, `instZero`, `module'`, `monoid`, `restrictAddMonoidHom`, `restrictMonoidHom`, `restrictRingHom`, `semigroup`, `semiring`	35
Theorems `add_comp`, `coeFnAddMonoidHom_apply`, `coeFnAlgHom_apply`, `coeFnLinearMap_apply`, `coeFnMonoidHom_apply`, `coeFnRingHom_apply`, `coe_add`, `coe_div`, `coe_inv`, `coe_mul`, `coe_neg`, `coe_nsmul`, `coe_one`, `coe_pow`, `coe_smul`, `coe_sub`, `coe_zero`, `mul_comp`, `smul_comp`, `smul_comp'`	20
Total	55

ContMDiffMap

Definitions

Name	Category	Theorems
`C` 📖	CompOp	—
`addCommGroup` 📖	CompOp	2 math math: `LeftInvariantDerivation.coe_neg`, `LeftInvariantDerivation.map_neg`
`addCommMonoid` 📖	CompOp	13 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`, `LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop`, `Derivation.evalAt_apply`, `coeFnLinearMap_apply`
`addGroup` 📖	CompOp	5 math math: `coe_sub`, `LeftInvariantDerivation.coe_sub`, `coe_neg`, `LeftInvariantDerivation.map_sub`, `LeftInvariantDerivation.commutator_apply`
`addMonoid` 📖	CompOp	2 math math: `coeFnAddMonoidHom_apply`, `LeftInvariantDerivation.coeFnAddMonoidHom_apply`
`addSemigroup` 📖	CompOp	—
`algebra` 📖	CompOp	1 math math: `coeFnAlgHom_apply`
`coeFnAddMonoidHom` 📖	CompOp	1 math math: `coeFnAddMonoidHom_apply`
`coeFnAlgHom` 📖	CompOp	1 math math: `coeFnAlgHom_apply`
`coeFnLinearMap` 📖	CompOp	1 math math: `coeFnLinearMap_apply`
`coeFnMonoidHom` 📖	CompOp	1 math math: `coeFnMonoidHom_apply`
`coeFnRingHom` 📖	CompOp	1 math math: `coeFnRingHom_apply`
`commGroup` 📖	CompOp	—
`commMonoid` 📖	CompOp	—
`commRing` 📖	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`
`compLeftAddMonoidHom` 📖	CompOp	—
`compLeftMonoidHom` 📖	CompOp	—
`compLeftRingHom` 📖	CompOp	—
`evalRingHom` 📖	CompOp	—
`group` 📖	CompOp	2 math math: `coe_div`, `coe_inv`
`instAdd` 📖	CompOp	5 math math: `LeftInvariantDerivation.leibniz`, `add_comp`, `coe_add`, `LeftInvariantDerivation.map_add`, `LeftInvariantDerivation.coe_add`
`instMul` 📖	CompOp	3 math math: `LeftInvariantDerivation.leibniz`, `coe_mul`, `mul_comp`
`instNSMul` 📖	CompOp	1 math math: `coe_nsmul`
`instOne` 📖	CompOp	1 math math: `coe_one`
`instPow` 📖	CompOp	1 math math: `coe_pow`
`instSMul` 📖	CompOp	6 math math: `smul_comp`, `coe_smul`, `LeftInvariantDerivation.map_smul`, `PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf`, `LeftInvariantDerivation.coe_smul`, `smooth_functions_tower`
`instSMul'` 📖	CompOp	3 math math: `LeftInvariantDerivation.leibniz`, `smul_comp'`, `smooth_functions_tower`
`instZero` 📖	CompOp	3 math math: `LeftInvariantDerivation.map_zero`, `coe_zero`, `LeftInvariantDerivation.coe_zero`
`module'` 📖	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`
`monoid` 📖	CompOp	1 math math: `coeFnMonoidHom_apply`
`restrictAddMonoidHom` 📖	CompOp	—
`restrictMonoidHom` 📖	CompOp	—
`restrictRingHom` 📖	CompOp	—
`semigroup` 📖	CompOp	—
`semiring` 📖	CompOp	8 math math: `coeFnAlgHom_apply`, `LeftInvariantDerivation.left_invariant'`, `LeftInvariantDerivation.lift_smul`, `LeftInvariantDerivation.evalAt_coe`, `LeftInvariantDerivation.left_invariant''`, `PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf`, `coeFnRingHom_apply`, `Derivation.evalAt_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_comp` 📖	mathematical	—	`comp` `ContMDiffMap` `instAdd`	—	—
`coeFnAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ContMDiffMap` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `addMonoid` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `coeFnAddMonoidHom` `instFunLike`	—	—
`coeFnAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `ContMDiffMap` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedRing.toSeminormedRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `chartedSpaceSelf` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `semiring` `Ring.toSemiring` `NormedRing.toRing` `Pi.semiring` `algebra` `Function.algebra` `NormedAlgebra.toAlgebra` `AlgHom.funLike` `coeFnAlgHom` `instFunLike`	—	—
`coeFnLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ContMDiffMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instContMDiffAddSelf` `Pi.addCommMonoid` `module` `Pi.Function.module` `NormedSpace.toModule` `LinearMap.instFunLike` `coeFnLinearMap` `instFunLike`	—	`instContMDiffAddSelf`
`coeFnMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `ContMDiffMap` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `monoid` `Pi.mulOneClass` `MonoidHom.instFunLike` `coeFnMonoidHom` `instFunLike`	—	—
`coeFnRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `ContMDiffMap` `Semiring.toNonAssocSemiring` `semiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.nonAssocSemiring` `RingHom.instFunLike` `coeFnRingHom` `instFunLike`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `instAdd` `Pi.instAdd`	—	—
`coe_div` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `group` `Pi.instDiv`	—	—
`coe_inv` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `group` `Pi.instInv`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `instMul` `Pi.instMul`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `addGroup` `Pi.instNeg`	—	—
`coe_nsmul` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `instNSMul` `Pi.instSMul` `AddMonoid.toNatSMul`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `instOne` `Pi.instOne`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `instPow` `Pi.instPow` `Monoid.toNatPow`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `addGroup` `Pi.instSub`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `ContMDiffMap` `instFunLike` `instZero` `Pi.instZero`	—	—
`mul_comp` 📖	mathematical	—	`comp` `ContMDiffMap` `instMul`	—	—
`smul_comp` 📖	mathematical	—	`comp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `ContMDiffMap` `instSMul`	—	—
`smul_comp'` 📖	mathematical	—	`comp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `ContMDiffMap` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instSMul'`	—	—

---

← Back to Index