TrivSqZeroExt

📁 Source: Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean

Statistics

Metric	Count
Definitions `instL1NormedAddCommGroup`, `instL1NormedAlgebra`, `instL1NormedCommRing`, `instL1NormedRing`, `instL1NormedSpace`, `instL1SeminormedAddCommGroup`, `instL1SeminormedCommRing`, `instL1SeminormedRing`	8
Theorems `eq_smul_exp_of_invertible`, `eq_smul_exp_of_ne_zero`, `exp_def`, `exp_def_of_smul_comm`, `exp_inl`, `exp_inr`, `fst_exp`, `fst_expSeries`, `hasSum_expSeries_of_smul_comm`, `hasSum_snd_expSeries_of_smul_comm`, `instL1IsBoundedSMul`, `instNormOneClass`, `nnnorm_def`, `nnnorm_inl`, `nnnorm_inr`, `norm_def`, `norm_inl`, `norm_inr`, `snd_exp`, `snd_expSeries_of_smul_comm`	20
Total	28

TrivSqZeroExt

Definitions

Name	Category	Theorems
`instL1NormedAddCommGroup` 📖	CompOp	—
`instL1NormedAlgebra` 📖	CompOp	—
`instL1NormedCommRing` 📖	CompOp	—
`instL1NormedRing` 📖	CompOp	—
`instL1NormedSpace` 📖	CompOp	—
`instL1SeminormedAddCommGroup` 📖	CompOp	6 math math: `norm_def`, `norm_inl`, `nnnorm_def`, `nnnorm_inl`, `nnnorm_inr`, `norm_inr`
`instL1SeminormedCommRing` 📖	CompOp	—
`instL1SeminormedRing` 📖	CompOp	2 math math: `instNormOneClass`, `instL1IsBoundedSMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_smul_exp_of_invertible` 📖	mathematical	—	`TrivSqZeroExt` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `fst` `NormedSpace.exp` `ring` `CommRing.toRing` `IsScalarTower.to_smulCommClass` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `IsScalarTower.op_right` `AddCommMonoid.toAddMonoid` `IsScalarTower.left` `DistribMulAction.toMulAction` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `Invertible.invOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `snd`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.op_right` `IsScalarTower.left` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `inr_smul` `exp_inr` `smul_add` `inl_one` `inl_smul` `smul_eq_mul` `mul_one` `smul_smul` `mul_invOf_self` `one_smul` `inl_fst_add_inr_snd_eq`
`eq_smul_exp_of_ne_zero` 📖	mathematical	—	`TrivSqZeroExt` `smul` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `fst` `NormedSpace.exp` `ring` `DivisionRing.toRing` `Field.toDivisionRing` `IsScalarTower.to_smulCommClass` `MulOpposite` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `IsScalarTower.op_right` `AddCommMonoid.toAddMonoid` `IsScalarTower.left` `DistribMulAction.toMulAction` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `snd`	—	`eq_smul_exp_of_invertible`
`exp_def` 📖	mathematical	—	`NormedSpace.exp` `TrivSqZeroExt` `ring` `CommRing.toRing` `IsScalarTower.to_smulCommClass` `CommRing.toCommSemiring` `MulOpposite` `MulOpposite.instSemiring` `CommSemiring.toSemiring` `MulOpposite.instAlgebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `IsScalarTower.op_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsScalarTower.left` `DistribMulAction.toMulAction` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `fst` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `snd`	—	`exp_def_of_smul_comm` `IsScalarTower.to_smulCommClass` `IsScalarTower.op_right` `IsScalarTower.left` `IsCentralScalar.op_smul_eq_smul`
`exp_def_of_smul_comm` 📖	mathematical	`MulOpposite` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `MulOpposite.instSemiring` `AddCommGroup.toAddCommMonoid` `MulOpposite.op` `fst` `snd`	`NormedSpace.exp` `TrivSqZeroExt` `ring` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `IsScalarTower.rat` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NormedSpace.exp_eq_expSeries_sum` `Rat.instCharZero` `HasSum.tsum_eq` `instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_expSeries_of_smul_comm` `Summable.hasSum` `tsum_eq_zero_of_not_summable` `zero_smul` `inr_zero` `inl_zero` `zero_add` `Summable.map` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `continuous_fst`
`exp_inl` 📖	mathematical	—	`NormedSpace.exp` `TrivSqZeroExt` `ring` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `exp_def_of_smul_comm` `snd_inl` `fst_inl` `smul_zero` `inr_zero` `add_zero`
`exp_inr` 📖	mathematical	—	`NormedSpace.exp` `TrivSqZeroExt` `ring` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `exp_def_of_smul_comm` `snd_inr` `fst_inr` `MulOpposite.op_zero` `zero_smul` `NormedSpace.exp_zero` `one_smul` `inl_one`
`fst_exp` 📖	mathematical	—	`fst` `NormedSpace.exp` `TrivSqZeroExt` `ring` `CommRing.toRing` `IsScalarTower.to_smulCommClass` `CommRing.toCommSemiring` `MulOpposite` `MulOpposite.instSemiring` `CommSemiring.toSemiring` `MulOpposite.instAlgebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `IsScalarTower.op_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsScalarTower.left` `DistribMulAction.toMulAction` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.op_right` `IsScalarTower.left` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `exp_def` `fst_add` `fst_inl` `fst_inr` `add_zero`
`fst_expSeries` 📖	mathematical	—	`fst` `DFunLike.coe` `ContinuousMultilinearMap` `TrivSqZeroExt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ring` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `algebra'` `AddCommGroup.toAddCommMonoid` `instTopologicalSpace` `ContinuousMultilinearMap.funLike` `NormedSpace.expSeries` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`	—	`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `NormedSpace.expSeries_apply_eq`
`hasSum_expSeries_of_smul_comm` 📖	mathematical	`MulOpposite` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `MulOpposite.instSemiring` `AddCommGroup.toAddCommMonoid` `MulOpposite.op` `fst` `snd` `HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.toModule` `Semifield.toCommSemiring` `ContinuousMultilinearMap.funLike` `NormedSpace.expSeries` `SummationFilter.unconditional`	`TrivSqZeroExt` `addCommMonoid` `instTopologicalSpace` `ring` `algebra'` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `fst_expSeries` `inl_fst_add_inr_snd_eq` `HasSum.add` `instContinuousAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalAddGroup.toContinuousAdd` `hasSum_inl` `hasSum_inr` `hasSum_snd_expSeries_of_smul_comm`
`hasSum_snd_expSeries_of_smul_comm` 📖	mathematical	`MulOpposite` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `MulOpposite.instSemiring` `AddCommGroup.toAddCommMonoid` `MulOpposite.op` `fst` `snd` `HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.toModule` `Semifield.toCommSemiring` `ContinuousMultilinearMap.funLike` `NormedSpace.expSeries` `SummationFilter.unconditional`	`TrivSqZeroExt` `ring` `algebra'` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`	—	`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `hasSum_nat_add_iff'` `snd_expSeries_of_smul_comm` `NormedSpace.expSeries_apply_eq` `Finset.sum_congr` `Finset.range_one` `Finset.sum_singleton` `Nat.factorial_zero` `Nat.cast_one` `pow_zero` `inv_one` `one_smul` `snd_one` `sub_zero` `HasSum.smul_const`
`instL1IsBoundedSMul` 📖	mathematical	—	`IsBoundedSMul` `TrivSqZeroExt` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `instL1SeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalSeminormedCommRing.toNonUnitalCommRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `zero` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smul` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`WithLp.isBoundedSMulSeminormedAddCommGroupToProd` `fact_one_le_one_ennreal`
`instNormOneClass` 📖	mathematical	—	`NormOneClass` `TrivSqZeroExt` `SeminormedRing.toNorm` `instL1SeminormedRing` `one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `SeminormedRing.toRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_def` `fst_one` `snd_one` `norm_zero` `NormOneClass.norm_one` `add_zero`
`nnnorm_def` 📖	mathematical	—	`NNNorm.nnnorm` `TrivSqZeroExt` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instL1SeminormedAddCommGroup` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `SeminormedRing.toNonUnitalSeminormedRing` `fst` `snd`	—	`NNReal.eq` `norm_def`
`nnnorm_inl` 📖	mathematical	—	`NNNorm.nnnorm` `TrivSqZeroExt` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instL1SeminormedAddCommGroup` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `SeminormedRing.toNonUnitalSeminormedRing`	—	`nnnorm_def` `nnnorm_zero` `add_zero`
`nnnorm_inr` 📖	mathematical	—	`NNNorm.nnnorm` `TrivSqZeroExt` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instL1SeminormedAddCommGroup` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing`	—	`nnnorm_def` `nnnorm_zero` `zero_add`
`norm_def` 📖	mathematical	—	`Norm.norm` `TrivSqZeroExt` `SeminormedAddCommGroup.toNorm` `instL1SeminormedAddCommGroup` `Real` `Real.instAdd` `SeminormedRing.toNorm` `fst` `snd`	—	`fact_one_le_one_ennreal` `WithLp.norm_seminormedAddCommGroupToProd` `WithLp.prod_norm_eq_add` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.rpow_one` `div_self`
`norm_inl` 📖	mathematical	—	`Norm.norm` `TrivSqZeroExt` `SeminormedAddCommGroup.toNorm` `instL1SeminormedAddCommGroup` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedRing.toNorm`	—	`norm_def` `norm_zero` `add_zero`
`norm_inr` 📖	mathematical	—	`Norm.norm` `TrivSqZeroExt` `SeminormedAddCommGroup.toNorm` `instL1SeminormedAddCommGroup` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing`	—	`norm_def` `norm_zero` `zero_add`
`snd_exp` 📖	mathematical	—	`snd` `NormedSpace.exp` `TrivSqZeroExt` `ring` `CommRing.toRing` `IsScalarTower.to_smulCommClass` `CommRing.toCommSemiring` `MulOpposite` `MulOpposite.instSemiring` `CommSemiring.toSemiring` `MulOpposite.instAlgebra` `Algebra.id` `AddCommGroup.toAddCommMonoid` `IsScalarTower.op_right` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `IsScalarTower.left` `DistribMulAction.toMulAction` `instTopologicalSpace` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `fst`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.op_right` `IsScalarTower.left` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `exp_def` `snd_add` `snd_inl` `snd_inr` `zero_add`
`snd_expSeries_of_smul_comm` 📖	mathematical	`MulOpposite` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulOpposite.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `MulOpposite.instSemiring` `AddCommGroup.toAddCommMonoid` `MulOpposite.op` `fst` `snd`	`DFunLike.coe` `ContinuousMultilinearMap` `TrivSqZeroExt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ring` `Algebra.toModule` `Semifield.toCommSemiring` `algebra'` `instTopologicalSpace` `ContinuousMultilinearMap.funLike` `NormedSpace.expSeries` `instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite`	—	`instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite` `NormedSpace.expSeries_apply_eq` `snd_pow_of_smul_comm` `Nat.cast_smul_eq_nsmul` `smul_smul` `smul_assoc` `Nat.cast_mul` `mul_inv_rev` `inv_mul_cancel_right₀` `Nat.cast_ne_zero`

---

← Back to Index