Theorems · Inductive type · functional analysis
NormMulClass
(α : Type u_5) → [Norm α] → [Mul α] → Prop
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
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Normstatement · cited by 512
Cited by75
Results whose statement or proof uses this declaration.
- norm_mulstatement and proof · cited by 171
- norm_powstatement and proof · cited by 106
- Submonoid.unitSpherestatement and proof · cited by 85
- Asymptotics.IsBigO.mulstatement and proof · cited by 29
- Asymptotics.IsBigO.mul_isLittleOstatement and proof · cited by 15
- norm_prodstatement and proof · cited by 13
- Asymptotics.IsLittleO.mul_isBigOstatement and proof · cited by 11
- nnnorm_mulstatement and proof · cited by 10
- normHomstatement and proof · cited by 8
- Asymptotics.IsBigO.powstatement and proof · cited by 8
- nnnorm_powstatement and proof · cited by 8
- nnnormHomstatement and proof · cited by 7