Commit 2023-10-19 22:16 0a44be31

View on Github →

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

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Block.lean

added theorem Matrix.blockTriangular_one

added theorem Matrix.blockTriangular_stdBasisMatrix'

added theorem Matrix.blockTriangular_stdBasisMatrix

added theorem Matrix.blockTriangular_transvection'

added theorem Matrix.blockTriangular_transvection