Theorem Matrix.isHyperbolic_conj'_iff

Modification history

2025-09-13 14:08
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
feat(NumberTheory/ModularForms): Cusps of subgroups acting on upper half-plane (#29327) …
Modified Matrix.isHyperbolic_conj'_iffView on Github →
2025-09-03 18:14
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
feat(Compactification/OnePoint): classify GL2 elements by fixed points (#28552) …
Added Matrix.isHyperbolic_conj'_iffView on Github →