Theorem Matrix.vecMul_stdBasis

Modification history

2024-08-03 13:28

Mathlib/LinearAlgebra/Matrix/ToLin.lean

chore: backports for leanprover/lean4#4814 (part 14) (#15406)

Modified Matrix.vecMul_stdBasis View on Github →

2023-04-28 03:54

Mathlib/LinearAlgebra/Matrix/ToLin.lean

feat: port LinearAlgebra.Matrix.ToLin (#3552)

Added Matrix.vecMul_stdBasis View on Github →