Theorem Matrix.IsParabolic.sub_eigenvalue_sq_eq_zero

Modification history

2025-09-03 18:14
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
feat(Compactification/OnePoint): classify GL2 elements by fixed points (#28552) …
Added Matrix.IsParabolic.sub_eigenvalue_sq_eq_zeroView on Github →