Structures · Analysis
NormMulClass
A mixin class for strict multiplicativity of the norm, ‖a * b‖ = ‖a‖ * ‖b‖ (rather than
≤ as in the definition of NormedRing). Many NormedRings satisfy this stronger property,
including all NormedDivisionRings and NormedFields.
- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Shape
- One type argument · adds norm_mul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Int
- PadicInt
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by82
- norm_mul
- norm_pow
- Submonoid.unitSphere
- Asymptotics.IsBigO.mul
- Asymptotics.IsBigO.mul_isLittleO
- norm_prod
- Asymptotics.IsLittleO.mul_isBigO
- nnnorm_mul
- nnnorm_pow
- normHom
- Asymptotics.IsBigO.pow
- nnnormHom
- Asymptotics.isBigO_self_const_mul
- Asymptotics.IsLittleO.const_mul_right
- enorm_mul
- Asymptotics.IsBigOWith.mul
- Asymptotics.IsLittleO.pow
- tendsto_pow_atTop_nhds_zero_iff_norm_lt_one
- Asymptotics.IsBigO.const_mul_right
- Asymptotics.isLittleO_pow_pow_cobounded_of_lt
- Asymptotics.IsBigOWith.pow'
- AddChar.norm_apply
- Asymptotics.isBigOWith_self_const_mul
- Dilation.mulRight
- Polynomial.isEquivalent_cobounded_leading_monomial
- IsOfFinOrder.norm_eq_one
- Asymptotics.IsBigOWith.of_pow
- Dilation.mulLeft
- PadicInt.continuousAddCharEquiv_of_norm_mul
- HasProd.norm
- nnnorm_prod
- Asymptotics.IsLittleO.mul
- Asymptotics.isBigO_pow_pow_cobounded_of_le
- Asymptotics.isBigO_const_mul_right_iff
- summable_norm_mul_geometric_of_norm_lt_one'
- Asymptotics.isLittleO_const_mul_left_iff
- NormMulClass.norm_mul
- nnnormHom_apply
- Summable.mul_tendsto_const
- NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero
- Multipliable.norm_tprod
- Asymptotics.isBigO_const_mul_left_iff
- tprod_one_add_ne_zero_of_summable
- Asymptotics.IsLittleO.of_pow
- NormedAlgebra.Complex.algEquivOfNormMul
- tendsto_pow_cobounded_cobounded
- Metric.unitSphere.coe_mul
- Asymptotics.isLittleO_const_mul_right_iff
- Asymptotics.IsBigOWith.const_mul_right
- Polynomial.isLittleO_cobounded_of_degree_lt
Ancestors0
No ancestors.