Theorem Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff

Modification history

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