Documentation Verification Report

RingSeminorm

📁 Source: Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

Statistics

Metric	Count
Definitions `MulRingNorm`, `funLike`, `instInhabited`, `instOne`, `mulRingNormEquivAbsoluteValue`, `toAddGroupNorm`, `toMulRingSeminorm`, `MulRingSeminorm`, `funLike`, `instInhabited`, `instOne`, `toAddGroupSeminorm`, `toMonoidWithZeroHom`, `toAbsoluteValue`, `toMulRingNorm`, `toRingNorm`, `RingNorm`, `funLike`, `instInhabitedOfDecidableEq`, `instOneOfDecidableEq`, `toAddGroupNorm`, `toNormedRing`, `toRingSeminorm`, `RingSeminorm`, `funLike`, `instInhabited`, `instOneOfDecidableEq`, `instZero`, `toAddGroupSeminorm`, `toRingNorm`, `toRingSeminorm`, `normRingNorm`, `normRingSeminorm`	33
Theorems `apply_one`, `eq_zero_of_map_eq_zero'`, `ext`, `ext_iff`, `mulRingNormClass`, `mulRingNormEquivAbsoluteValue_apply`, `mulRingNormEquivAbsoluteValue_symm_apply`, `toFun_eq_coe`, `apply_one`, `ext`, `ext_iff`, `map_mul'`, `map_one'`, `mulRingSeminormClass`, `toFun_eq_coe`, `toRingNorm_apply`, `toRingNorm_toFun`, `apply_one`, `eq_zero_of_map_eq_zero'`, `ext`, `ext_iff`, `ringNormClass`, `toFun_eq_coe`, `apply_one`, `eq_zero_iff`, `exists_index_pow_le`, `ext`, `ext_iff`, `isBoundedUnder`, `mul_le'`, `ne_zero_iff`, `ringSeminormClass`, `seminorm_one_eq_one_iff_ne_zero`, `toFun_eq_coe`, `toRingSeminorm_apply`, `map_pow_le_pow`, `map_pow_le_pow'`, `normRingNorm_toFun`	38
Total	71

MulRingNorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	7 math math: `ext_iff`, `mulRingNormClass`, `mulRingNormEquivAbsoluteValue_symm_apply`, `toFun_eq_coe`, `mulRingNormEquivAbsoluteValue_apply`, `isPowMul`, `apply_one`
`instInhabited` 📖	CompOp	—
`instOne` 📖	CompOp	1 math math: `apply_one`
`mulRingNormEquivAbsoluteValue` 📖	CompOp	2 math math: `mulRingNormEquivAbsoluteValue_symm_apply`, `mulRingNormEquivAbsoluteValue_apply`
`toAddGroupNorm` 📖	CompOp	—
`toMulRingSeminorm` 📖	CompOp	3 math math: `MulAlgebraNorm.toFun_eq_coe`, `toFun_eq_coe`, `MulAlgebraNorm.smul'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_one` 📖	mathematical	—	`DFunLike.coe` `MulRingNorm` `Real` `funLike` `instOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Real.instZero` `Real.instOne`	—	—
`eq_zero_of_map_eq_zero'` 📖	mathematical	`AddGroupSeminorm.toFun` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `MulRingSeminorm.toAddGroupSeminorm` `toMulRingSeminorm` `Real` `Real.instZero`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`ext` 📖	—	`DFunLike.coe` `MulRingNorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `MulRingNorm` `Real` `funLike`	—	`ext`
`mulRingNormClass` 📖	mathematical	—	`MulRingNormClass` `MulRingNorm` `Real` `Real.semiring` `Real.partialOrder` `funLike`	—	`AddGroupSeminorm.add_le'` `AddGroupSeminorm.map_zero'` `AddGroupSeminorm.neg'` `MulRingSeminorm.map_mul'` `MulRingSeminorm.map_one'` `eq_zero_of_map_eq_zero'`
`mulRingNormEquivAbsoluteValue_apply` 📖	mathematical	—	`DFunLike.coe` `AbsoluteValue` `Real` `Ring.toSemiring` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Equiv` `MulRingNorm` `Ring.toNonAssocRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `mulRingNormEquivAbsoluteValue` `funLike`	—	—
`mulRingNormEquivAbsoluteValue_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulRingNorm` `Ring.toNonAssocRing` `Real` `funLike` `Equiv` `AbsoluteValue` `Ring.toSemiring` `Real.semiring` `Real.partialOrder` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `mulRingNormEquivAbsoluteValue` `AbsoluteValue.funLike`	—	—
`toFun_eq_coe` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `MulRingSeminorm.toAddGroupSeminorm` `toMulRingSeminorm` `DFunLike.coe` `MulRingNorm` `Real` `funLike`	—	—

MulRingSeminorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	4 math math: `apply_one`, `mulRingSeminormClass`, `toFun_eq_coe`, `ext_iff`
`instInhabited` 📖	CompOp	—
`instOne` 📖	CompOp	1 math math: `apply_one`
`toAddGroupSeminorm` 📖	CompOp	6 math math: `map_mul'`, `MulAlgebraNorm.toFun_eq_coe`, `MulRingNorm.toFun_eq_coe`, `toFun_eq_coe`, `map_one'`, `MulAlgebraNorm.smul'`
`toMonoidWithZeroHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_one` 📖	mathematical	—	`DFunLike.coe` `MulRingSeminorm` `Real` `funLike` `instOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Real.instZero` `Real.instOne`	—	—
`ext` 📖	—	`DFunLike.coe` `MulRingSeminorm` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `MulRingSeminorm` `Real` `funLike`	—	`ext`
`map_mul'` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toAddGroupSeminorm` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Real` `Semiring.toNonAssocSemiring` `Real.semiring`	—	—
`map_one'` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toAddGroupSeminorm` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Real` `Semiring.toNonAssocSemiring` `Real.semiring`	—	—
`mulRingSeminormClass` 📖	mathematical	—	`MulRingSeminormClass` `MulRingSeminorm` `Real` `Real.semiring` `Real.partialOrder` `funLike`	—	`AddGroupSeminorm.add_le'` `AddGroupSeminorm.map_zero'` `AddGroupSeminorm.neg'` `map_mul'` `map_one'`
`toFun_eq_coe` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Real` `AddGroupSeminorm.funLike` `toAddGroupSeminorm` `MulRingSeminorm` `funLike`	—	—

NormedField

Definitions

Name	Category	Theorems
`toAbsoluteValue` 📖	CompOp	—
`toMulRingNorm` 📖	CompOp	—

NormedRing

Definitions

Name	Category	Theorems
`toRingNorm` 📖	CompOp	2 math math: `toRingNorm_toFun`, `toRingNorm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toRingNorm_apply` 📖	mathematical	—	`DFunLike.coe` `RingNorm` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Real` `RingNorm.funLike` `NonUnitalNormedRing.toNonUnitalRing` `toNonUnitalNormedRing` `toRingNorm` `Norm.norm` `toNorm`	—	—
`toRingNorm_toFun` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `RingSeminorm.toAddGroupSeminorm` `RingNorm.toRingSeminorm` `toRingNorm` `Norm.norm` `toNorm`	—	—

RingNorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	6 math math: `apply_one`, `toFun_eq_coe`, `ringNormClass`, `ext_iff`, `NormedRing.toRingNorm_apply`, `seminormFromConstRingNormOfField_def`
`instInhabitedOfDecidableEq` 📖	CompOp	—
`instOneOfDecidableEq` 📖	CompOp	1 math math: `apply_one`
`toAddGroupNorm` 📖	CompOp	—
`toNormedRing` 📖	CompOp	—
`toRingSeminorm` 📖	CompOp	5 math math: `NormedRing.toRingNorm_toFun`, `AlgebraNorm.smul'`, `AlgebraNorm.toFun_eq_coe`, `normRingNorm_toFun`, `toFun_eq_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_one` 📖	mathematical	—	`DFunLike.coe` `RingNorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `funLike` `instOneOfDecidableEq` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Real.instZero` `Real.instOne`	—	—
`eq_zero_of_map_eq_zero'` 📖	mathematical	`AddGroupSeminorm.toFun` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `RingSeminorm.toAddGroupSeminorm` `toRingSeminorm` `Real` `Real.instZero`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`ext` 📖	—	`DFunLike.coe` `RingNorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingNorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `funLike`	—	`ext`
`ringNormClass` 📖	mathematical	—	`RingNormClass` `RingNorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `Real.semiring` `Real.partialOrder` `funLike`	—	`AddGroupSeminorm.add_le'` `AddGroupSeminorm.map_zero'` `AddGroupSeminorm.neg'` `RingSeminorm.mul_le'` `eq_zero_of_map_eq_zero'`
`toFun_eq_coe` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `RingSeminorm.toAddGroupSeminorm` `toRingSeminorm` `DFunLike.coe` `RingNorm` `Real` `funLike`	—	—

RingSeminorm

Definitions

Name	Category	Theorems
`funLike` 📖	CompOp	11 math math: `ringSeminormClass`, `smoothingFun_le`, `eq_zero_iff`, `toFun_eq_coe`, `smoothingFun_le_self`, `zero_mem_lowerBounds_smoothingSeminormSeq_range`, `smoothingSeminormSeq_bddBelow`, `ext_iff`, `apply_one`, `SeminormedRing.toRingSeminorm_apply`, `seminormFromConst_seq_def`
`instInhabited` 📖	CompOp	—
`instOneOfDecidableEq` 📖	CompOp	1 math math: `apply_one`
`instZero` 📖	CompOp	1 math math: `eq_zero_iff`
`toAddGroupSeminorm` 📖	CompOp	7 math math: `NormedRing.toRingNorm_toFun`, `AlgebraNorm.smul'`, `AlgebraNorm.toFun_eq_coe`, `normRingNorm_toFun`, `mul_le'`, `RingNorm.toFun_eq_coe`, `toFun_eq_coe`
`toRingNorm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_one` 📖	mathematical	—	`DFunLike.coe` `RingSeminorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `funLike` `instOneOfDecidableEq` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Real.instZero` `Real.instOne`	—	—
`eq_zero_iff` 📖	mathematical	—	`RingSeminorm` `NonUnitalRing.toNonUnitalNonAssocRing` `instZero` `DFunLike.coe` `Real` `funLike` `Real.instZero`	—	`DFunLike.ext_iff`
`exists_index_pow_le` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingSeminorm` `funLike` `NonUnitalCommRing.toNonUnitalRing`	`Real.instLE` `Real.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Real.instMul`	—	`IsNonarchimedean.add_pow_le` `AddGroupSeminormClass.toZeroHomClass` `RingSeminormClass.toAddGroupSeminormClass` `ringSeminormClass` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `RingSeminormClass.toSubmultiplicativeHomClass` `Real.rpow_le_rpow` `NonnegHomClass.apply_nonneg` `Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass`
`ext` 📖	—	`DFunLike.coe` `RingSeminorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RingSeminorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `funLike`	—	`ext`
`isBoundedUnder` 📖	mathematical	`Real` `Real.instLE` `DFunLike.coe` `RingSeminorm` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `funLike` `Ring.toNonUnitalRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instOne`	`Filter.IsBoundedUnder` `Filter.atTop` `Nat.instPreorder` `Real.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`mul_one_div` `Real.rpow_mul` `NonnegHomClass.apply_nonneg` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `ringSeminormClass` `Real.rpow_natCast` `le_imp_le_of_le_of_le` `Real.rpow_le_rpow` `map_pow_le_pow'` `Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass` `le_refl` `Filter.isBoundedUnder_of` `le_or_gt` `le_trans` `Real.rpow_le_one` `div_nonneg` `Real.rpow_le_self_of_one_le` `LT.lt.le` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `RCLike.charZero_rclike` `Nat.cast_nonneg`
`mul_le'` 📖	mathematical	—	`Real` `Real.instLE` `AddGroupSeminorm.toFun` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `toAddGroupSeminorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Real.instMul`	—	—
`ne_zero_iff` 📖	—	—	—	—	—
`ringSeminormClass` 📖	mathematical	—	`RingSeminormClass` `RingSeminorm` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `Real.semiring` `Real.partialOrder` `funLike`	—	`AddGroupSeminorm.add_le'` `AddGroupSeminorm.map_zero'` `AddGroupSeminorm.neg'` `mul_le'`
`seminorm_one_eq_one_iff_ne_zero` 📖	—	`Real` `Real.instLE` `DFunLike.coe` `RingSeminorm` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `funLike` `Ring.toNonUnitalRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instOne`	—	—	`ne_zero_iff` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `LE.le.eq_or_lt'` `NonnegHomClass.apply_nonneg` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `ringSeminormClass` `ext` `LE.le.antisymm'` `mul_one` `MulZeroClass.mul_zero` `SubmultiplicativeHomClass.map_mul_le_mul` `RingSeminormClass.toSubmultiplicativeHomClass` `LE.le.antisymm` `le_mul_iff_one_le_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `one_mul`
`toFun_eq_coe` 📖	mathematical	—	`DFunLike.coe` `AddGroupSeminorm` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `Real` `AddGroupSeminorm.funLike` `toAddGroupSeminorm` `RingSeminorm` `funLike`	—	—

SeminormedRing

Definitions

Name	Category	Theorems
`toRingSeminorm` 📖	CompOp	1 math math: `toRingSeminorm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toRingSeminorm_apply` 📖	mathematical	—	`DFunLike.coe` `RingSeminorm` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Real` `RingSeminorm.funLike` `NonUnitalSeminormedRing.toNonUnitalRing` `toNonUnitalSeminormedRing` `toRingSeminorm` `Norm.norm` `toNorm`	—	—

(root)

Definitions

Name	Category	Theorems
`MulRingNorm` 📖	CompData	7 math math: `MulRingNorm.ext_iff`, `MulRingNorm.mulRingNormClass`, `MulRingNorm.mulRingNormEquivAbsoluteValue_symm_apply`, `MulRingNorm.toFun_eq_coe`, `MulRingNorm.mulRingNormEquivAbsoluteValue_apply`, `MulRingNorm.isPowMul`, `MulRingNorm.apply_one`
`MulRingSeminorm` 📖	CompData	4 math math: `MulRingSeminorm.apply_one`, `MulRingSeminorm.mulRingSeminormClass`, `MulRingSeminorm.toFun_eq_coe`, `MulRingSeminorm.ext_iff`
`RingNorm` 📖	CompData	6 math math: `RingNorm.apply_one`, `RingNorm.toFun_eq_coe`, `RingNorm.ringNormClass`, `RingNorm.ext_iff`, `NormedRing.toRingNorm_apply`, `seminormFromConstRingNormOfField_def`
`RingSeminorm` 📖	CompData	11 math math: `RingSeminorm.ringSeminormClass`, `smoothingFun_le`, `RingSeminorm.eq_zero_iff`, `RingSeminorm.toFun_eq_coe`, `smoothingFun_le_self`, `zero_mem_lowerBounds_smoothingSeminormSeq_range`, `smoothingSeminormSeq_bddBelow`, `RingSeminorm.ext_iff`, `RingSeminorm.apply_one`, `SeminormedRing.toRingSeminorm_apply`, `seminormFromConst_seq_def`
`normRingNorm` 📖	CompOp	1 math math: `normRingNorm_toFun`
`normRingSeminorm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_pow_le_pow` 📖	mathematical	—	`Real` `Real.instLE` `DFunLike.coe` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Real.instMonoid`	—	`pow_one` `pow_succ` `le_imp_le_of_le_of_le` `SubmultiplicativeHomClass.map_mul_le_mul` `RingSeminormClass.toSubmultiplicativeHomClass` `le_refl` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `NonnegHomClass.apply_nonneg` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid`
`map_pow_le_pow'` 📖	mathematical	`Real` `Real.instLE` `DFunLike.coe` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instOne`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Real.instMonoid`	—	`pow_zero` `map_pow_le_pow`
`normRingNorm_toFun` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `RingSeminorm.toAddGroupSeminorm` `RingNorm.toRingSeminorm` `normRingNorm` `Norm.norm` `SeminormedAddGroup.toNorm` `NormedAddGroup.toSeminormedAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup`	—	—

---

← Back to Index