Theorem Matrix.blockTriangular_stdBasisMatrix'

Modification history

2025-05-06 15:16

Mathlib/LinearAlgebra/Matrix/Block.lean

refactor: rename `Matrix.stdBasisMatrix` to `Matrix.single` (#24622) …

Deleted Matrix.blockTriangular_stdBasisMatrix'View on Github →

2023-10-19 22:16

Mathlib/LinearAlgebra/Matrix/Block.lean

feat(LinearAlgebra/Matrix): transvection matrix is block triangular (#7765)

Added Matrix.blockTriangular_stdBasisMatrix'View on Github →