Theorem OrthogonalFamily.norm_sq_sdiff_sum

Modification history

2026-06-09 08:51
Mathlib/Analysis/InnerProductSpace/Subspace.lean
chore: rename `diff` to `sdiff` (#40184) …
Added OrthogonalFamily.norm_sq_sdiff_sumView on Github →