Theorem OrthonormalBasis.reindex_toBasis

Modification history

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