Theorems · Theorem · functional analysis
norm_eq_zero
∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, ‖a‖ = 0 ↔ a = 0- Defined in
- Mathlib.Analysis.Normed.Group.Basic
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedAddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Norm.normstatement · cited by 5,413
- norm_nonnegproof · cited by 725
- LE.le.ge_iff_eq'proof · cited by 50
- NormedAddGroupstatement and proof · cited by 32
- norm_le_zero_iffproof · cited by 23
Cited by43
Results whose statement or proof uses this declaration.
- norm_ne_zero_iffproof · cited by 65
- inner_self_eq_zeroproof · cited by 18
- MeromorphicOn.circleIntegrable_log_normproof · cited by 11
- MeasureTheory.DominatedFinMeasAdditive.eq_zero_of_measure_zeroproof · cited by 9
- nnnorm_eq_zeroproof · cited by 6
- eq_zero_or_norm_posproof · cited by 6
- LinearMap.normDet_eq_zero_iff_ker_ne_botproof · cited by 5
- Affine.Simplex.ExcenterExists.touchpoint_injectiveproof · cited by 4
- norm_sub_eq_zero_iffproof · cited by 4
- MeromorphicOn.extract_zeros_poles_logproof · cited by 3
- Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eqproof · cited by 3
- sameRay_iff_of_norm_eqproof · cited by 3