Theorem OrthonormalBasis.sum_sq_norm_inner

Modification history

2025-06-23 13:09
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: lemmas about orthonormal bases (#26276) …
Deleted OrthonormalBasis.sum_sq_norm_innerView on Github →
2025-04-07 13:30
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat(MeasureTheory): tightness criterion in finite dimensional inner product spaces (#23534) …
Added OrthonormalBasis.sum_sq_norm_innerView on Github →