Theorem WithLp.equiv_symm_eq_zero_iff

Modification history

2026-01-01 15:17
Mathlib/Analysis/Normed/Lp/WithLp.lean
chore: remove June 2025 deprecated declarations (#33429) …
Deleted WithLp.equiv_symm_eq_zero_iffView on Github →
2025-06-07 02:30
Mathlib/Analysis/Normed/Lp/WithLp.lean
feat: simp lemmas for WithLp eq zero (#25552) …
Added WithLp.equiv_symm_eq_zero_iffView on Github →