Theorem Matrix.charpoly_of_upperTriangular

Modification history

2026-07-30 16:24
Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
feat(LinearAlgebra/Matrix): add definitions and theory for the echelon form and pivots of matrices (#42236) …
Deleted Matrix.charpoly_of_upperTriangularView on Github →
2024-10-26 16:21
Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
feat(Matrix): characteristic polynomial of upper triangular matrix (#17338) …
Added Matrix.charpoly_of_upperTriangularView on Github →