Theorem OrthonormalBasis.inner_eq_ite

Modification history

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