Theorems · Inductive type · functional analysis
NormedGroup
Type u_8 → Type u_8
A normed group is a group endowed with a norm for which dist x y = ‖x⁻¹ * y‖ defines a metric
space structure.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by37
Results whose statement or proof uses this declaration.
- norm_eq_zero'statement and proof · cited by 4
- norm_le_zero_iff'statement and proof · cited by 3
- norm_div_eq_zero_iffstatement and proof · cited by 2
- norm_pos_iff'statement and proof · cited by 2
- nnnorm_eq_zero'statement and proof · cited by 1
- GroupNormClass.toNormedCommGroupproof · cited by 1
- GroupNormClass.toNormedGroupstatement · cited by 1
- nnnorm_ne_zero_iff'statement and proof · cited by 1
- eq_one_or_norm_posstatement and proof · cited by 1
- tendsto_norm_inv_mul_self_nhdsNEstatement and proof · cited by 1
- normGroupNormstatement and proof · cited by 1
- eq_of_norm_div_eq_zerostatement and proof · cited by 0