Theorem Matrix.blockTriangular_transvection

Modification history

2023-10-19 22:16

Mathlib/LinearAlgebra/Matrix/Block.lean

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

Added Matrix.blockTriangular_transvection View on Github →