Theorems · Definition · functional analysis
Norm.norm
{E : Type u_8} → [self : Norm E] → E → ℝthe ℝ-valued norm function.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 5,413 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- Norm
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by5,827
Results whose statement or proof uses this declaration.
- norm_nonnegstatement · cited by 725
- norm_zerostatement · cited by 366
- norm_smulstatement · cited by 242
- Complex.argproof · cited by 220
- norm_negstatement and proof · cited by 190
- Complex.logproof · cited by 187
- dist_eq_normstatement · cited by 182
- PadicIntproof · cited by 179
- dist_zero_rightstatement and proof · cited by 172
- norm_mulstatement · cited by 171
- InnerProductGeometry.angleproof · cited by 170
- norm_pos_iffstatement · cited by 168
Showing the 200 most cited of 5,827.