Theorems · Inductive type · functional analysis
NormOneClass
(α : Type u_5) → [Norm α] → [One α] → Prop
A mixin class with the axiom ‖1‖ = 1. Many NormedRings and all NormedFields satisfy this
axiom.
- Defined in
- Mathlib.Analysis.Normed.Ring.Basic
- Cited by
- 136 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · 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 by147
Results whose statement or proof uses this declaration.
- NormOneClass.norm_onestatement and proof · cited by 148
- norm_powstatement and proof · cited by 106
- Submonoid.unitSpherestatement and proof · cited by 85
- norm_algebraMap'statement and proof · cited by 39
- enorm_onestatement and proof · cited by 26
- Asymptotics.isLittleO_one_iffstatement and proof · cited by 20
- norm_prodstatement and proof · cited by 13
- nnnorm_onestatement and proof · cited by 11
- spectrum.norm_le_norm_of_memstatement and proof · cited by 11
- Filter.Tendsto.isBigO_onestatement and proof · cited by 10
- Asymptotics.IsBigO.powstatement and proof · cited by 8
- nnnorm_powstatement and proof · cited by 8