Theorem OrthonormalBasis.sum_sq_norm_inner_left

Modification history

2025-06-23 13:09
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: lemmas about orthonormal bases (#26276) …
Added OrthonormalBasis.sum_sq_norm_inner_leftView on Github →