Commit 2025-06-07 02:30 994033ef

View on Github →

feat: simp lemmas for WithLp eq zero (#25552) zulip discussion: #new members > EuclideanSpace.single 2 1 ≠ 0

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

added theorem EuclideanSpace.single_eq_zero_iff

Modified Mathlib/Analysis/Normed/Lp/WithLp.lean

added theorem WithLp.equiv_eq_zero_iff

added theorem WithLp.equiv_symm_eq_zero_iff