IsPowMulFaithful

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

Statistics

Metric	Count
Definitions	0
Theorems contraction_of_isPowMul, contraction_of_isPowMul_of_boundedWrt, eq_of_powMul_faithful, eq_seminorms	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contraction_of_isPowMul 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Norm.norm SeminormedRing.toNorm RingHom.IsBounded	Real Real.instLE DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	contraction_of_isPowMul_of_boundedWrt RingSeminorm.ringSeminormClass
contraction_of_isPowMul_of_boundedWrt 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring RingHom.IsBoundedWrt DFunLike.coe Real	Real.instLE RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	one_mul Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.comp ContinuousAt.tendsto Real.continuousAt_const_rpow ne_of_gt Real.rpow_zero tendsto_const_div_atTop_nhds_zero_nat RCLike.charZero_rclike NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero NNRat.instContinuousSMulRatReal tendsto_const_nhds ge_of_tendsto instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Nat.cast_ne_zero Real.rpow_natCast Real.rpow_mul le_of_lt one_div inv_mul_cancel₀ Real.rpow_one le_of_pow_le_pow_left₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono Real.rpow_nonneg NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass mul_pow map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass le_trans mul_le_mul_iff_right₀ PosMulStrictMono.toPosMulReflectLE map_pow_le_pow
eq_of_powMul_faithful 📖	—	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing CommRing.toRing Real AlgebraNorm.instFunLikeReal Real.instLE Subalgebra NormedCommRing.toCommRing SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet Real.instMul	—	—	AlgebraNorm.ext SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass IsPowMul.restriction Algebra.self_mem_adjoin_singleton eq_seminorms RingNormClass.toRingSeminormClass AlgebraNormClass.toRingNormClass AlgebraNorm.algebraNormClass
eq_seminorms 📖	—	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring DFunLike.coe Real Real.instLE Real.instMul	—	—	DFunLike.coe_injective' le_antisymm contraction_of_isPowMul_of_boundedWrt

---

← Back to Index