Theorem Pi.orthonormalBasis_repr

Modification history

2024-06-13 00:50
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: Define `Pi.orthonormalBasis` (#12242) …
Added Pi.orthonormalBasis_reprView on Github →