Theorem Matrix.charmatrix_blockTriangular_iff

Modification history

2024-10-26 16:21
Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
feat(Matrix): characteristic polynomial of upper triangular matrix (#17338) …
Added Matrix.charmatrix_blockTriangular_iffView on Github →