Theorem Pi.orthonormalBasis_apply

Modification history

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