Documentation Verification Report

SuperpolynomialDecay

📁 Source: Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

Statistics

Metric	Count
Definitions `SuperpolynomialDecay`	1
Theorems `add`, `congr'`, `const_mul`, `inv_param_mul`, `mul`, `mul_const`, `mul_param`, `mul_param_pow`, `mul_param_zpow`, `mul_polynomial`, `param_inv_mul`, `param_mul`, `param_pow_mul`, `param_zpow_mul`, `polynomial_mul`, `trans_abs_le`, `trans_eventuallyLE`, `trans_eventually_abs_le`, `superpolynomialDecay_const_mul_iff`, `superpolynomialDecay_iff_abs_isBoundedUnder`, `superpolynomialDecay_iff_abs_tendsto_zero`, `superpolynomialDecay_iff_isBigO`, `superpolynomialDecay_iff_isLittleO`, `superpolynomialDecay_iff_norm_tendsto_zero`, `superpolynomialDecay_iff_superpolynomialDecay_abs`, `superpolynomialDecay_iff_superpolynomialDecay_norm`, `superpolynomialDecay_iff_zpow_tendsto_zero`, `superpolynomialDecay_mul_const_iff`, `superpolynomialDecay_mul_param_iff`, `superpolynomialDecay_mul_param_pow_iff`, `superpolynomialDecay_param_mul_iff`, `superpolynomialDecay_param_pow_mul_iff`, `superpolynomialDecay_zero`	33
Total	34

Asymptotics

Definitions

Name	Category	Theorems
`SuperpolynomialDecay` 📖	MathDef	15 math math: `superpolynomialDecay_iff_zpow_tendsto_zero`, `superpolynomialDecay_zero`, `superpolynomialDecay_iff_isLittleO`, `superpolynomialDecay_iff_abs_isBoundedUnder`, `superpolynomialDecay_mul_param_pow_iff`, `superpolynomialDecay_iff_isBigO`, `superpolynomialDecay_iff_norm_tendsto_zero`, `superpolynomialDecay_mul_const_iff`, `superpolynomialDecay_param_mul_iff`, `superpolynomialDecay_iff_superpolynomialDecay_abs`, `superpolynomialDecay_const_mul_iff`, `superpolynomialDecay_param_pow_mul_iff`, `superpolynomialDecay_iff_abs_tendsto_zero`, `superpolynomialDecay_mul_param_iff`, `superpolynomialDecay_iff_superpolynomialDecay_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`superpolynomialDecay_const_mul_iff` 📖	mathematical	—	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`SuperpolynomialDecay.congr` `SuperpolynomialDecay.const_mul` `inv_mul_cancel₀` `one_mul`
`superpolynomialDecay_iff_abs_isBoundedUnder` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Filter.IsBoundedUnder` `Preorder.toLE` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Filter.Tendsto.isBoundedUnder_le` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Filter.Tendsto.abs` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `superpolynomialDecay_iff_abs_tendsto_zero` `tendsto_const_nhds` `Filter.Tendsto.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `IsStrictOrderedRing.toIsTopologicalDivisionRing` `tendsto_zero_iff_abs_tendsto_zero` `Filter.Tendsto.inv_tendsto_atTop` `MulZeroClass.zero_mul` `tendsto_of_tendsto_of_tendsto_of_le_of_le'` `Filter.Eventually.of_forall` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `Filter.Eventually.mp` `Filter.eventually_map` `Filter.Eventually.mono` `Filter.Tendsto.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Eq.trans_le` `abs_mul` `mul_assoc` `pow_succ'` `inv_mul_cancel₀` `one_mul` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono`
`superpolynomialDecay_iff_abs_tendsto_zero` 📖	mathematical	—	`SuperpolynomialDecay` `CommRing.toCommSemiring` `Filter.Tendsto` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`tendsto_zero_iff_abs_tendsto_zero` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`superpolynomialDecay_iff_isBigO` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `IsBigO` `NormedField.toNorm` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`superpolynomialDecay_iff_zpow_tendsto_zero` `Filter.Tendsto.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `isBigO_of_div_tendsto_nhds` `Filter.Eventually.mono` `zpow_ne_zero` `zpow_neg` `div_eq_mul_inv` `mul_comm` `IsBigO.trans` `IsBigO.mul` `NormedDivisionRing.toNormMulClass` `isBigO_refl` `IsBigO.of_bound'` `neg_add_rev` `zpow_add₀` `add_neg_cancel_comm_assoc` `zpow_one` `norm_inv` `IsBigO.trans_tendsto` `Filter.Tendsto.inv_tendsto_atTop`
`superpolynomialDecay_iff_isLittleO` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `IsLittleO` `NormedField.toNorm` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing`	—	`Filter.Tendsto.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `isLittleO_of_tendsto'` `Filter.Eventually.mono` `one_div` `Filter.Tendsto.inv_tendsto_atTop` `one_mul` `IsLittleO.mul_isBigO` `NormedDivisionRing.toNormMulClass` `superpolynomialDecay_iff_isBigO` `IsLittleO.trans_isBigO` `IsBigO.of_bound'` `le_of_eq` `zpow_one_add₀` `add_sub_cancel` `norm_zpow` `IsLittleO.isBigO`
`superpolynomialDecay_iff_norm_tendsto_zero` 📖	mathematical	—	`SuperpolynomialDecay` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Filter.Tendsto` `Real` `Norm.norm` `NormedField.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `nhds` `Real.pseudoMetricSpace` `Real.instZero`	—	`tendsto_zero_iff_norm_tendsto_zero`
`superpolynomialDecay_iff_superpolynomialDecay_abs` 📖	mathematical	—	`SuperpolynomialDecay` `CommRing.toCommSemiring` `abs` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`superpolynomialDecay_iff_abs_tendsto_zero` `abs_mul` `IsStrictOrderedRing.toIsOrderedRing` `abs_pow`
`superpolynomialDecay_iff_superpolynomialDecay_norm` 📖	mathematical	—	`SuperpolynomialDecay` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real` `Real.pseudoMetricSpace` `Real.instCommSemiring` `Norm.norm` `NormedField.toNorm`	—	`superpolynomialDecay_iff_norm_tendsto_zero` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass`
`superpolynomialDecay_iff_zpow_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_natCast` `Filter.Tendsto.comp` `tendsto_zpow_atTop_zero` `pow_zero` `one_mul` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `IsStrictOrderedRing.toIsTopologicalDivisionRing` `MulZeroClass.zero_mul`
`superpolynomialDecay_mul_const_iff` 📖	mathematical	—	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`SuperpolynomialDecay.congr` `SuperpolynomialDecay.mul_const` `mul_assoc` `mul_inv_cancel₀` `mul_one`
`superpolynomialDecay_mul_param_iff` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mul_comm` `superpolynomialDecay_param_mul_iff`
`superpolynomialDecay_mul_param_pow_iff` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`mul_comm` `superpolynomialDecay_param_pow_mul_iff`
`superpolynomialDecay_param_mul_iff` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`SuperpolynomialDecay.congr'` `SuperpolynomialDecay.inv_param_mul` `Filter.Eventually.mono` `Filter.Tendsto.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `inv_mul_cancel₀` `one_mul` `SuperpolynomialDecay.param_mul`
`superpolynomialDecay_param_pow_mul_iff` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`pow_zero` `one_mul` `pow_succ` `mul_comm` `mul_assoc` `superpolynomialDecay_param_mul_iff`
`superpolynomialDecay_zero` 📖	mathematical	—	`SuperpolynomialDecay` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`MulZeroClass.mul_zero` `tendsto_const_nhds`

Asymptotics.SuperpolynomialDecay

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`mul_add` `Distrib.leftDistribClass` `add_zero` `Filter.Tendsto.add`
`congr'` 📖	—	`Asymptotics.SuperpolynomialDecay` `Filter.EventuallyEq`	—	—	`Filter.Tendsto.congr'` `Filter.EventuallyEq.mul` `Filter.EventuallyEq.refl`
`const_mul` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`congr` `mul_const` `mul_comm`
`inv_param_mul` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Asymptotics.SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`zpow_neg` `zpow_one` `param_zpow_mul`
`mul` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`pow_zero` `one_mul` `mul_assoc` `MulZeroClass.mul_zero` `Filter.Tendsto.mul`
`mul_const` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`MulZeroClass.zero_mul` `Filter.Tendsto.mul_const`
`mul_param` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`congr` `param_mul` `mul_comm`
`mul_param_pow` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`congr` `param_pow_mul` `mul_comm`
`mul_param_zpow` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Asymptotics.SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`congr` `param_zpow_mul` `mul_comm`
`mul_polynomial` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Polynomial.eval`	—	`congr` `polynomial_mul` `mul_comm`
`param_inv_mul` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Asymptotics.SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`congr` `inv_param_mul` `mul_comm`
`param_mul` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`tendsto_nhds` `Filter.sets_of_superset`
`param_pow_mul` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_zero` `one_mul` `pow_succ'` `mul_assoc` `param_mul`
`param_zpow_mul` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Asymptotics.SuperpolynomialDecay` `Semifield.toCommSemiring` `Field.toSemifield`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero` `Filter.Tendsto.congr'` `Filter.Eventually.mono` `Filter.Tendsto.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `zpow_add₀` `mul_assoc`
`polynomial_mul` 📖	mathematical	`Asymptotics.SuperpolynomialDecay`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Polynomial.eval`	—	`Polynomial.induction_on'` `Polynomial.eval_add` `add_mul` `Distrib.rightDistribClass` `add` `Polynomial.eval_monomial` `mul_assoc` `const_mul` `param_pow_mul`
`trans_abs_le` 📖	—	`Asymptotics.SuperpolynomialDecay` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—	`trans_eventually_abs_le` `Filter.Eventually.of_forall`
`trans_eventuallyLE` 📖	—	`Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Asymptotics.SuperpolynomialDecay`	—	—	`tendsto_of_tendsto_of_tendsto_of_le_of_le'` `Filter.mp_mem` `Filter.univ_mem'` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass`
`trans_eventually_abs_le` 📖	—	`Asymptotics.SuperpolynomialDecay` `CommRing.toCommSemiring` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—	`Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero` `tendsto_of_tendsto_of_tendsto_of_le_of_le'` `tendsto_const_nhds` `Filter.Eventually.of_forall` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `Filter.Eventually.mono` `abs_mul` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono`

---

← Back to Index