Theorem Basis.toMatrix_mulVec_repr

Modification history

2025-07-24 16:31
Mathlib/LinearAlgebra/Matrix/Basis.lean
chore: rename `Basis` to `Module.Basis` (#27381) …
Deleted Basis.toMatrix_mulVec_reprView on Github →
2025-02-15 09:40
Mathlib/LinearAlgebra/Matrix/Basis.lean
chore(LinearAlgebra): fix some `Fintype`/`DecidableEq` (#21898) …
Modified Basis.toMatrix_mulVec_reprView on Github →
2024-11-28 16:12
Mathlib/LinearAlgebra/Matrix/Basis.lean
feat: drop finite-dimensionality assumption from `PerfectPairing.restrictScalarsField` (#18940)
Added Basis.toMatrix_mulVec_reprView on Github →