Commit 2025-07-03 03:52 5e176975

View on Github →

feat(NumberTheory/ModularForms): GL(2, R) action preserves holomorphy (#25894) Show that the slash action of negative-determinant matrices preserves holomorphic functions.

Estimated changes

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

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

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

added def UpperHalfPlane.J

added theorem UpperHalfPlane.J_smul

added theorem UpperHalfPlane.J_sq

added theorem UpperHalfPlane.coe_J_smul

added theorem UpperHalfPlane.denom_J

added theorem UpperHalfPlane.det_J

added theorem UpperHalfPlane.sigma_J

added theorem UpperHalfPlane.val_J