Theorem OrthonormalBasis.inner_eq_one

Modification history

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