Commit 2025-09-03 18:14 1a776ad6

View on Github →

feat(Compactification/OnePoint): classify GL2 elements by fixed points (#28552) Classify 2x2 matrices over R as elliptic, parabolic or hyperbolic and describe their fixed points.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

added theorem Matrix.charpoly_fin_two

added theorem Matrix.charpoly_of_card_eq_two

Created Mathlib/LinearAlgebra/Matrix/Charpoly/Disc.lean

added theorem Matrix.disc_fin_two

added theorem Matrix.disc_of_card_eq_two

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Basic.lean

added theorem Matrix.GeneralLinearGroup.center_eq_range_units

added theorem Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar

Created Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean

added theorem Matrix.GeneralLinearGroup.IsParabolic.pow

added theorem Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff

added theorem Matrix.GeneralLinearGroup.parabolicEigenvalue_ne_zero

added def Matrix.IsElliptic

added def Matrix.IsHyperbolic

added theorem Matrix.IsParabolic.sub_eigenvalue_sq_eq_zero

added def Matrix.IsParabolic

added theorem Matrix.disc_conj'

added theorem Matrix.disc_conj

added theorem Matrix.isElliptic_conj'_iff

added theorem Matrix.isElliptic_conj_iff

added theorem Matrix.isHyperbolic_conj'_iff

added theorem Matrix.isHyperbolic_conj_iff

added theorem Matrix.isParabolic_conj'_iff

added theorem Matrix.isParabolic_conj_iff

added theorem Matrix.isParabolic_iff_exists

added def Matrix.parabolicEigenvalue

added theorem Matrix.sub_scalar_sq_eq_disc

Modified Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean

added theorem Matrix.GeneralLinearGroup.IsElliptic.smul_ne_self

added theorem Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow

added theorem Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff

added theorem Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff

added def Matrix.GeneralLinearGroup.parabolicFixedPoint

added theorem OnePoint.map_smul

modified theorem OnePoint.smul_infty_def

deleted theorem OnePoint.smul_infty_eq_iff

added theorem OnePoint.smul_infty_eq_self_iff

modified theorem OnePoint.smul_some_eq_ite