Theorem Pi.orthonormalBasis.toBasis

Modification history

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