Theorems · Theorem · functional analysis
WithLp.toLp_eq_zero
∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] {x : V}, WithLp.toLp p x = 0 ↔ x = 0- Defined in
- Mathlib.Analysis.Normed.Lp.WithLp
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- ENNRealstatement and proof · cited by 9,879
- WithLpstatement · cited by 345
- WithLp.toLp_injectiveproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- MeasureTheory.volume_sum_rpow_lt_oneproof · cited by 2
- Complex.volume_sum_rpow_lt_oneproof · cited by 1
- RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zeroproof · cited by 1
- Complex.volume_sum_rpow_leproof · cited by 0
- PiLp.single_eq_zero_iffproof · cited by 0
- MeasureTheory.volume_sum_rpow_leproof · cited by 0