Monoid

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

Statistics

Metric	Count
Definitions ContMDiffAdd, ContMDiffAddMonoidMorphism, toAddMonoidHom, ContMDiffMonoidMorphism, toMonoidHom, ContMDiffMul, Design_choices_about_smooth_algebraic_structures, «term𝑳», «term𝑹», instFunLikeContMDiffAddMonoidMorphism, instFunLikeContMDiffMonoidMorphism, instInhabitedContMDiffAddMonoidMorphism, instInhabitedContMDiffMonoidMorphism, instOneContMDiffMonoidMorphism, instZeroContMDiffAddMonoidMorphism, smoothLeftMul, smoothRightMul	17
Theorems add, div_const, mul, nsmul, pow, prod, sub_const, sum, contMDiff_add, of_le, prod, toIsManifold, contMDiff_toFun, add, div_const, mul, nsmul, pow, prod, sub_const, sum, contMDiff_toFun, contMDiff_mul, of_le, prod, toIsManifold, add, div_const, mul, nsmul, pow, sub_const, add, div_const, mul, nsmul, pow, prod, sub_const, sum, L_apply, L_mul, R_apply, R_mul, contMDiffAt_add_left, contMDiffAt_add_right, contMDiffAt_finprod, contMDiffAt_finset_prod, contMDiffAt_finset_prod', contMDiffAt_finset_sum, contMDiffAt_finset_sum', contMDiffAt_finsum, contMDiffAt_mul_left, contMDiffAt_mul_right, contMDiffOn_finprod, contMDiffOn_finset_prod, contMDiffOn_finset_prod', contMDiffOn_finset_sum, contMDiffOn_finset_sum', contMDiffOn_finsum, contMDiffWithinAt_finprod, contMDiffWithinAt_finset_prod, contMDiffWithinAt_finset_prod', contMDiffWithinAt_finset_sum, contMDiffWithinAt_finset_sum', contMDiffWithinAt_finsum, contMDiff_add, contMDiff_add_left, contMDiff_add_right, contMDiff_finprod, contMDiff_finprod_cond, contMDiff_finset_prod, contMDiff_finset_prod', contMDiff_finset_sum, contMDiff_finset_sum', contMDiff_finsum, contMDiff_finsum_cond, contMDiff_mul, contMDiff_mul_left, contMDiff_mul_right, contMDiff_nsmul, contMDiff_pow, continuousAdd_of_contMDiffAdd, continuousMul_of_contMDiffMul, instAddMonoidHomClassContMDiffAddMonoidMorphism, instContMDiffAddOfNatWithTopENat, instContMDiffAddOfNatWithTopENatOfContinuousAdd, instContMDiffAddOfSomeENatTopOfLEInfty, instContMDiffAddOfTopWithTopENat, instContMDiffAddSelf, instContMDiffMulOfNatWithTopENat, instContMDiffMulOfNatWithTopENatOfContinuousMul, instContMDiffMulOfSomeENatTopOfLEInfty, instContMDiffMulOfTopWithTopENat, instContinuousMapClassContMDiffAddMonoidMorphism, instContinuousMapClassContMDiffMonoidMorphism, instMonoidHomClassContMDiffMonoidMorphism, mdifferentiableAt_add_left, mdifferentiableAt_add_right, mdifferentiableAt_mul_left, mdifferentiableAt_mul_right, mdifferentiable_add_left, mdifferentiable_add_right, mdifferentiable_mul_left, mdifferentiable_mul_right, smoothLeftMul_one, smoothRightMul_one	107
Total	124

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	ContMDiff	ContMDiff Pi.instAdd	—	ContMDiffAt.add
div_const 📖	mathematical	ContMDiff	ContMDiff DivInvMonoid.toDiv	—	ContMDiffAt.div_const
mul 📖	mathematical	ContMDiff	ContMDiff Pi.instMul	—	ContMDiffAt.mul
nsmul 📖	mathematical	ContMDiff	ContMDiff AddMonoid.toNSMul AddCommMonoid.toAddMonoid	—	ContMDiffAt.nsmul
pow 📖	mathematical	ContMDiff	ContMDiff Monoid.toPow CommMonoid.toMonoid	—	ContMDiffAt.pow
prod 📖	mathematical	ContMDiff	ContMDiff Finset.prod	—	ContMDiffAt.prod
sub_const 📖	mathematical	ContMDiff	ContMDiff SubNegMonoid.toSub	—	ContMDiffAt.sub_const
sum 📖	mathematical	ContMDiff	ContMDiff Finset.sum	—	ContMDiffAt.sum

ContMDiffAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiff_add 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace	—	—
of_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	ContMDiffAdd	—	IsManifold.of_le toIsManifold ContMDiff.of_le contMDiff_add
prod 📖	mathematical	—	ContMDiffAdd ModelProd instTopologicalSpaceModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelWithCorners.prod Prod.instAdd instTopologicalSpaceProd prodChartedSpace	—	IsManifold.prod toIsManifold ContMDiff.prodMk ContMDiff.add ContMDiff.comp contMDiff_fst contMDiff_snd
toIsManifold 📖	mathematical	—	IsManifold	—	—

ContMDiffAddMonoidMorphism

Definitions

Name	Category	Theorems
toAddMonoidHom 📖	CompOp	1 math math: contMDiff_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiff_toFun 📖	mathematical	—	ContMDiff ZeroHom.toFun AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.toZeroHom toAddMonoidHom	—	—

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	ContMDiffAt	ContMDiffAt Pi.instAdd	—	ContMDiffWithinAt.add
div_const 📖	mathematical	ContMDiffAt	ContMDiffAt DivInvMonoid.toDiv	—	ContMDiffWithinAt.div_const
mul 📖	mathematical	ContMDiffAt	ContMDiffAt Pi.instMul	—	ContMDiffWithinAt.mul
nsmul 📖	mathematical	ContMDiffAt	ContMDiffAt AddMonoid.toNSMul AddCommMonoid.toAddMonoid	—	ContMDiffWithinAt.nsmul
pow 📖	mathematical	ContMDiffAt	ContMDiffAt Monoid.toPow CommMonoid.toMonoid	—	ContMDiffWithinAt.pow
prod 📖	mathematical	ContMDiffAt	ContMDiffAt Finset.prod	—	ContMDiffWithinAt.prod
sub_const 📖	mathematical	ContMDiffAt	ContMDiffAt SubNegMonoid.toSub	—	ContMDiffWithinAt.sub_const
sum 📖	mathematical	ContMDiffAt	ContMDiffAt Finset.sum	—	contMDiffWithinAt_univ ContMDiffWithinAt.sum

ContMDiffMonoidMorphism

Definitions

Name	Category	Theorems
toMonoidHom 📖	CompOp	1 math math: contMDiff_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiff_toFun 📖	mathematical	—	ContMDiff OneHom.toFun MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.toOneHom toMonoidHom	—	—

ContMDiffMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiff_mul 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace	—	—
of_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	ContMDiffMul	—	IsManifold.of_le toIsManifold ContMDiff.of_le contMDiff_mul
prod 📖	mathematical	—	ContMDiffMul ModelProd instTopologicalSpaceModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelWithCorners.prod Prod.instMul instTopologicalSpaceProd prodChartedSpace	—	IsManifold.prod toIsManifold ContMDiff.prodMk ContMDiff.mul ContMDiff.comp contMDiff_fst contMDiff_snd
toIsManifold 📖	mathematical	—	IsManifold	—	—

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	ContMDiffOn	ContMDiffOn Pi.instAdd	—	ContMDiffWithinAt.add
div_const 📖	mathematical	ContMDiffOn	ContMDiffOn DivInvMonoid.toDiv	—	ContMDiffWithinAt.div_const
mul 📖	mathematical	ContMDiffOn	ContMDiffOn Pi.instMul	—	ContMDiffWithinAt.mul
nsmul 📖	mathematical	ContMDiffOn	ContMDiffOn AddMonoid.toNSMul AddCommMonoid.toAddMonoid	—	ContMDiffWithinAt.nsmul
pow 📖	mathematical	ContMDiffOn	ContMDiffOn Monoid.toPow CommMonoid.toMonoid	—	ContMDiffWithinAt.pow
sub_const 📖	mathematical	ContMDiffOn	ContMDiffOn SubNegMonoid.toSub	—	ContMDiffWithinAt.sub_const

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Pi.instAdd	—	ContMDiffAt.comp_contMDiffWithinAt ContMDiff.contMDiffAt contMDiff_add prodMk
div_const 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt DivInvMonoid.toDiv	—	div_eq_mul_inv mul contMDiffWithinAt_const
mul 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Pi.instMul	—	ContMDiffAt.comp_contMDiffWithinAt ContMDiff.contMDiffAt contMDiff_mul prodMk
nsmul 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt AddMonoid.toNSMul AddCommMonoid.toAddMonoid	—	ContMDiffAt.comp_contMDiffWithinAt ContMDiff.contMDiffAt contMDiff_nsmul
pow 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Monoid.toPow CommMonoid.toMonoid	—	ContMDiffAt.comp_contMDiffWithinAt ContMDiff.contMDiffAt contMDiff_pow
prod 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Finset.prod	—	Finset.induction_on Finset.prod_insert mul Finset.mem_insert_self Finset.mem_insert_of_mem
sub_const 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt SubNegMonoid.toSub	—	sub_eq_add_neg add contMDiffWithinAt_const
sum 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Finset.sum	—	Finset.induction_on contMDiffWithinAt_const Finset.sum_insert add Finset.mem_insert_self Finset.mem_insert_of_mem

LibraryNote

Definitions

Name	Category	Theorems
Design_choices_about_smooth_algebraic_structures 📖	CompOp	—

LieGroup

Definitions

Name	Category	Theorems
«term𝑳» 📖	CompOp	—
«term𝑹» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ContMDiffAdd 📖	CompData	9 math math: instContMDiffAddOfNatWithTopENatOfContinuousAdd, ContMDiffAdd.prod, instContMDiffAddSelf, ContMDiffRing.toContMDiffAdd, instContMDiffAddOfSomeENatTopOfLEInfty, LieAddGroup.toContMDiffAdd, instContMDiffAddOfTopWithTopENat, ContMDiffAdd.of_le, instContMDiffAddOfNatWithTopENat
ContMDiffAddMonoidMorphism 📖	CompData	2 math math: instContinuousMapClassContMDiffAddMonoidMorphism, instAddMonoidHomClassContMDiffAddMonoidMorphism
ContMDiffMonoidMorphism 📖	CompData	2 math math: instContinuousMapClassContMDiffMonoidMorphism, instMonoidHomClassContMDiffMonoidMorphism
ContMDiffMul 📖	CompData	8 math math: ContMDiffMul.prod, ContMDiffMul.of_le, instContMDiffMulOfSomeENatTopOfLEInfty, instContMDiffMulOfNatWithTopENat, ContMDiffRing.toContMDiffMul, instContMDiffMulOfNatWithTopENatOfContinuousMul, instContMDiffMulOfTopWithTopENat, LieGroup.toContMDiffMul
instFunLikeContMDiffAddMonoidMorphism 📖	CompOp	2 math math: instContinuousMapClassContMDiffAddMonoidMorphism, instAddMonoidHomClassContMDiffAddMonoidMorphism
instFunLikeContMDiffMonoidMorphism 📖	CompOp	2 math math: instContinuousMapClassContMDiffMonoidMorphism, instMonoidHomClassContMDiffMonoidMorphism
instInhabitedContMDiffAddMonoidMorphism 📖	CompOp	—
instInhabitedContMDiffMonoidMorphism 📖	CompOp	—
instOneContMDiffMonoidMorphism 📖	CompOp	—
instZeroContMDiffAddMonoidMorphism 📖	CompOp	—
smoothLeftMul 📖	CompOp	8 math math: LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, LeftInvariantDerivation.comp_L, L_mul, LeftInvariantDerivation.left_invariant'', smoothLeftMul_one, L_apply, LeftInvariantDerivation.evalAt_mul
smoothRightMul 📖	CompOp	3 math math: smoothRightMul_one, R_mul, R_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
L_apply 📖	mathematical	—	DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike smoothLeftMul	—	—
L_mul 📖	mathematical	—	smoothLeftMul Semigroup.toMul ContMDiffMap.comp WithTop.some ENat Top.top instTopENat	—	ContMDiffMap.ext mul_assoc
R_apply 📖	mathematical	—	DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike smoothRightMul	—	—
R_mul 📖	mathematical	—	smoothRightMul Semigroup.toMul ContMDiffMap.comp WithTop.some ENat Top.top instTopENat	—	ContMDiffMap.ext mul_assoc
contMDiffAt_add_left 📖	mathematical	—	ContMDiffAt	—	ContMDiff.contMDiffAt contMDiff_add_left
contMDiffAt_add_right 📖	mathematical	—	ContMDiffAt	—	ContMDiff.contMDiffAt contMDiff_add_right
contMDiffAt_finprod 📖	mathematical	LocallyFinite Function.mulSupport MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid ContMDiffAt	ContMDiffAt finprod	—	contMDiffWithinAt_finprod
contMDiffAt_finset_prod 📖	mathematical	ContMDiffAt	ContMDiffAt Finset.prod	—	contMDiffWithinAt_finset_prod
contMDiffAt_finset_prod' 📖	mathematical	ContMDiffAt	ContMDiffAt Finset.prod Pi.commMonoid	—	contMDiffWithinAt_finset_prod'
contMDiffAt_finset_sum 📖	mathematical	ContMDiffAt	ContMDiffAt Finset.sum	—	contMDiffWithinAt_finset_sum
contMDiffAt_finset_sum' 📖	mathematical	ContMDiffAt	ContMDiffAt Finset.sum Pi.addCommMonoid	—	contMDiffWithinAt_finset_sum'
contMDiffAt_finsum 📖	mathematical	LocallyFinite Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ContMDiffAt	ContMDiffAt finsum	—	contMDiffWithinAt_finsum
contMDiffAt_mul_left 📖	mathematical	—	ContMDiffAt	—	ContMDiff.contMDiffAt contMDiff_mul_left
contMDiffAt_mul_right 📖	mathematical	—	ContMDiffAt	—	ContMDiff.contMDiffAt contMDiff_mul_right
contMDiffOn_finprod 📖	mathematical	LocallyFinite Function.mulSupport MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid ContMDiffOn	ContMDiffOn finprod	—	contMDiffWithinAt_finprod
contMDiffOn_finset_prod 📖	mathematical	ContMDiffOn	ContMDiffOn Finset.prod	—	contMDiffWithinAt_finset_prod
contMDiffOn_finset_prod' 📖	mathematical	ContMDiffOn	ContMDiffOn Finset.prod Pi.commMonoid	—	contMDiffWithinAt_finset_prod'
contMDiffOn_finset_sum 📖	mathematical	ContMDiffOn	ContMDiffOn Finset.sum	—	contMDiffWithinAt_finset_sum
contMDiffOn_finset_sum' 📖	mathematical	ContMDiffOn	ContMDiffOn Finset.sum Pi.addCommMonoid	—	contMDiffWithinAt_finset_sum'
contMDiffOn_finsum 📖	mathematical	LocallyFinite Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ContMDiffOn	ContMDiffOn finsum	—	contMDiffWithinAt_finsum
contMDiffWithinAt_finprod 📖	mathematical	LocallyFinite Function.mulSupport MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid ContMDiffWithinAt	ContMDiffWithinAt finprod	—	finprod_eventually_eq_prod ContMDiffWithinAt.congr_of_eventuallyEq ContMDiffWithinAt.prod eventually_nhdsWithin_of_eventually_nhds Filter.Eventually.self_of_nhds
contMDiffWithinAt_finset_prod 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Finset.prod	—	contMDiffWithinAt_finset_prod'
contMDiffWithinAt_finset_prod' 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Finset.prod Pi.commMonoid	—	Finset.prod_induction ContMDiffWithinAt.mul contMDiffWithinAt_const
contMDiffWithinAt_finset_sum 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Finset.sum	—	Finset.sum_apply contMDiffWithinAt_finset_sum'
contMDiffWithinAt_finset_sum' 📖	mathematical	ContMDiffWithinAt	ContMDiffWithinAt Finset.sum Pi.addCommMonoid	—	Finset.sum_induction ContMDiffWithinAt.add contMDiffWithinAt_const
contMDiffWithinAt_finsum 📖	mathematical	LocallyFinite Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid ContMDiffWithinAt	ContMDiffWithinAt finsum	—	finsum_eventually_eq_sum ContMDiffWithinAt.congr_of_eventuallyEq ContMDiffWithinAt.sum eventually_nhdsWithin_of_eventually_nhds Filter.Eventually.self_of_nhds
contMDiff_add 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace	—	ContMDiffAdd.contMDiff_add
contMDiff_add_left 📖	mathematical	—	ContMDiff	—	ContMDiff.add contMDiff_const contMDiff_id
contMDiff_add_right 📖	mathematical	—	ContMDiff	—	ContMDiff.add contMDiff_id contMDiff_const
contMDiff_finprod 📖	mathematical	ContMDiff LocallyFinite Function.mulSupport MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	ContMDiff finprod	—	contMDiffAt_finprod
contMDiff_finprod_cond 📖	mathematical	ContMDiff LocallyFinite Function.mulSupport MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	ContMDiff finprod	—	contMDiff_finprod LocallyFinite.comp_injective Subtype.coe_injective
contMDiff_finset_prod 📖	mathematical	ContMDiff	ContMDiff Finset.prod	—	contMDiffAt_finset_prod
contMDiff_finset_prod' 📖	mathematical	ContMDiff	ContMDiff Finset.prod Pi.commMonoid	—	contMDiffAt_finset_prod'
contMDiff_finset_sum 📖	mathematical	ContMDiff	ContMDiff Finset.sum	—	contMDiffAt_finset_sum
contMDiff_finset_sum' 📖	mathematical	ContMDiff	ContMDiff Finset.sum Pi.addCommMonoid	—	contMDiffAt_finset_sum'
contMDiff_finsum 📖	mathematical	ContMDiff LocallyFinite Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	ContMDiff finsum	—	contMDiffAt_finsum
contMDiff_finsum_cond 📖	mathematical	ContMDiff LocallyFinite Function.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	ContMDiff finsum	—	finsum_subtype_eq_finsum_cond contMDiff_finsum LocallyFinite.comp_injective Subtype.coe_injective
contMDiff_mul 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace	—	ContMDiffMul.contMDiff_mul
contMDiff_mul_left 📖	mathematical	—	ContMDiff	—	ContMDiff.mul contMDiff_const contMDiff_id
contMDiff_mul_right 📖	mathematical	—	ContMDiff	—	ContMDiff.mul contMDiff_id contMDiff_const
contMDiff_nsmul 📖	mathematical	—	ContMDiff AddMonoid.toNSMul	—	zero_nsmul contMDiff_const succ_nsmul ContMDiff.add contMDiff_id
contMDiff_pow 📖	mathematical	—	ContMDiff Monoid.toPow	—	pow_zero pow_succ ContMDiff.mul contMDiff_id
continuousAdd_of_contMDiffAdd 📖	mathematical	—	ContinuousAdd	—	ContMDiff.continuous contMDiff_add
continuousMul_of_contMDiffMul 📖	mathematical	—	ContinuousMul	—	ContMDiff.continuous contMDiff_mul
instAddMonoidHomClassContMDiffAddMonoidMorphism 📖	mathematical	—	AddMonoidHomClass ContMDiffAddMonoidMorphism AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLikeContMDiffAddMonoidMorphism	—	AddMonoidHom.map_add AddMonoidHom.map_zero
instContMDiffAddOfNatWithTopENat 📖	mathematical	—	ContMDiffAdd WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Nat.instAtLeastTwoHAddOfNat ContMDiffAdd.of_le one_le_two WithTop.zeroLEOneClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
instContMDiffAddOfNatWithTopENatOfContinuousAdd 📖	mathematical	—	ContMDiffAdd WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	IsManifold.instOfNatWithTopENat contMDiff_zero_iff continuous_add
instContMDiffAddOfSomeENatTopOfLEInfty 📖	mathematical	—	ContMDiffAdd	—	ContMDiffAdd.of_le ENat.LEInfty.out
instContMDiffAddOfTopWithTopENat 📖	mathematical	—	ContMDiffAdd	—	ContMDiffAdd.of_le le_top
instContMDiffAddSelf 📖	mathematical	—	ContMDiffAdd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid chartedSpaceSelf	—	IsManifold.instOfTopWithTopENat instIsManifoldModelSpace modelWithCornersSelf_prod chartedSpaceSelf_prod ContDiff.contMDiff contDiff_add
instContMDiffMulOfNatWithTopENat 📖	mathematical	—	ContMDiffMul WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Nat.instAtLeastTwoHAddOfNat ContMDiffMul.of_le one_le_two WithTop.zeroLEOneClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
instContMDiffMulOfNatWithTopENatOfContinuousMul 📖	mathematical	—	ContMDiffMul WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	IsManifold.instOfNatWithTopENat contMDiff_zero_iff continuous_mul
instContMDiffMulOfSomeENatTopOfLEInfty 📖	mathematical	—	ContMDiffMul	—	ContMDiffMul.of_le ENat.LEInfty.out
instContMDiffMulOfTopWithTopENat 📖	mathematical	—	ContMDiffMul	—	ContMDiffMul.of_le le_top
instContinuousMapClassContMDiffAddMonoidMorphism 📖	mathematical	—	ContinuousMapClass ContMDiffAddMonoidMorphism instFunLikeContMDiffAddMonoidMorphism	—	ContMDiff.continuous ContMDiffAddMonoidMorphism.contMDiff_toFun
instContinuousMapClassContMDiffMonoidMorphism 📖	mathematical	—	ContinuousMapClass ContMDiffMonoidMorphism instFunLikeContMDiffMonoidMorphism	—	ContMDiff.continuous ContMDiffMonoidMorphism.contMDiff_toFun
instMonoidHomClassContMDiffMonoidMorphism 📖	mathematical	—	MonoidHomClass ContMDiffMonoidMorphism MulOneClass.toMulOne Monoid.toMulOneClass instFunLikeContMDiffMonoidMorphism	—	MonoidHom.map_mul MonoidHom.map_one
mdifferentiableAt_add_left 📖	mathematical	—	MDifferentiableAt	—	ContMDiffAt.mdifferentiableAt contMDiffAt_add_left one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiableAt_add_right 📖	mathematical	—	MDifferentiableAt	—	ContMDiffAt.mdifferentiableAt contMDiffAt_add_right one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiableAt_mul_left 📖	mathematical	—	MDifferentiableAt	—	ContMDiffAt.mdifferentiableAt contMDiffAt_mul_left one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiableAt_mul_right 📖	mathematical	—	MDifferentiableAt	—	ContMDiffAt.mdifferentiableAt contMDiffAt_mul_right one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_add_left 📖	mathematical	—	MDifferentiable	—	ContMDiff.mdifferentiable contMDiff_add_left one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_add_right 📖	mathematical	—	MDifferentiable	—	ContMDiff.mdifferentiable contMDiff_add_right one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_mul_left 📖	mathematical	—	MDifferentiable	—	ContMDiff.mdifferentiable contMDiff_mul_left one_ne_zero NeZero.charZero_one WithTop.charZero
mdifferentiable_mul_right 📖	mathematical	—	MDifferentiable	—	ContMDiff.mdifferentiable contMDiff_mul_right one_ne_zero NeZero.charZero_one WithTop.charZero
smoothLeftMul_one 📖	mathematical	—	DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike smoothLeftMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	mul_one
smoothRightMul_one 📖	mathematical	—	DFunLike.coe ContMDiffMap WithTop.some ENat Top.top instTopENat ContMDiffMap.instFunLike smoothRightMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	one_mul

---

← Back to Index