Commit 2026-05-13 03:36 1c1dadbc

View on Github →

feat(UpperHalfPlane): define PGL action on the upper half-plane (#36330)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean

added theorem UpperHalfPlane.exists_gl_smul_eq_self_iff_trace_eq_zero

added def UpperHalfPlane.fixedPt

added theorem UpperHalfPlane.fixedPt_neg

added theorem UpperHalfPlane.forall_smul_eq_self_iff_mem_center

added theorem UpperHalfPlane.gl_smul_I_eq_I_iff_of_neg

added theorem UpperHalfPlane.gl_smul_I_eq_I_iff_of_pos

added theorem UpperHalfPlane.gl_smul_eq_iff_num_eq

added theorem UpperHalfPlane.gl_smul_eq_self_iff_dist_eq

added theorem UpperHalfPlane.gl_smul_eq_self_iff_dist_sq_eq

added theorem UpperHalfPlane.gl_smul_eq_self_iff_eq_fixedPt

added theorem UpperHalfPlane.gl_smul_eq_self_iff_quadratic

added theorem UpperHalfPlane.gl_smul_eq_self_iff_re_eq

added theorem UpperHalfPlane.isElliptic_of_exists_smul_eq_self

Modified Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

added theorem UpperHalfPlane.denom_scalar

added theorem UpperHalfPlane.glScalar_smul

added theorem UpperHalfPlane.num_one

added theorem UpperHalfPlane.num_scalar

added theorem UpperHalfPlane.pglMk_smul

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

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

added theorem Matrix.discr_conj'

added theorem Matrix.discr_conj

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

added theorem Matrix.IsElliptic.b_ne_zero

added theorem Matrix.IsElliptic.bc_ne_zero

added theorem Matrix.IsElliptic.c_ne_zero

added theorem Matrix.IsParabolic.neg

added theorem Matrix.IsParabolic.of_neg

deleted theorem Matrix.discr_conj'

deleted theorem Matrix.discr_conj

added theorem Matrix.isElliptic_neg_iff

added theorem Matrix.isHyperbolic_neg_iff

added theorem Matrix.isParabolic_neg_iff

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

added theorem Matrix.ProjGenLinGroup.mk_eq_one

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