Theorem Matrix.blockTriangular_one

Modification history

2024-12-16 14:33
Mathlib/LinearAlgebra/Matrix/Block.lean
feat(LinearAlgebra): general transitivity of norm (#19978) …
Modified Matrix.blockTriangular_oneView on Github →
2023-10-19 22:16
Mathlib/LinearAlgebra/Matrix/Block.lean
feat(LinearAlgebra/Matrix): transvection matrix is block triangular (#7765)
Added Matrix.blockTriangular_oneView on Github →