Theorem EuclideanSpace.single_eq_zero_iff

Modification history

2025-06-07 02:30
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: simp lemmas for WithLp eq zero (#25552) …
Added EuclideanSpace.single_eq_zero_iffView on Github →