Commit 2024-10-31 13:42 e7f74d3c

View on Github →

refactor (NumberTheory/ModularForms, Analysis/Complex/UpperHalfPlane) Refactor and clean up coercions (#18385) The code for SL(2, Z) and modular forms had lots of custom local notations, repeated in each file, for certain chains of coercions. We get rid of many of these, and harmonise the remaining ones using scoped (rather than file-local) notations. Separately, we get rid of a lot of annoying duplicate API lemmas by avoiding using subgroups as subtypes unless absolutely necessary.

Estimated changes

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

added theorem UpperHalfPlane.ModularGroup.coe_one

deleted theorem UpperHalfPlane.ModularGroup.subgroup_moeb

deleted theorem UpperHalfPlane.ModularGroup.subgroup_on_SL_apply

deleted theorem UpperHalfPlane.ModularGroup.subgroup_on_glpos_smul_apply

deleted theorem UpperHalfPlane.ModularGroup.subgroup_to_sl_moeb

modified def UpperHalfPlane.denom

modified theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero

modified theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero

modified def UpperHalfPlane.num

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

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

modified theorem Matrix.SpecialLinearGroup.coe_inv

modified theorem Matrix.SpecialLinearGroup.coe_one

modified theorem Matrix.SpecialLinearGroup.ext

modified theorem Matrix.SpecialLinearGroup.ext_iff

modified theorem Matrix.SpecialLinearGroup.row_ne_zero

modified theorem ModularGroup.S_mul_S_eq

modified theorem ModularGroup.T_inv_mul_apply_one

modified theorem ModularGroup.T_mul_apply_one

modified theorem ModularGroup.T_pow_mul_apply_one

modified theorem ModularGroup.coe_S

modified theorem ModularGroup.coe_T

modified theorem ModularGroup.coe_T_inv

modified theorem ModularGroup.coe_T_zpow

Modified Mathlib/NumberTheory/Modular.lean

modified theorem ModularGroup.abs_c_le_one

modified theorem ModularGroup.c_eq_zero

modified theorem ModularGroup.exists_eq_T_zpow_of_c_eq_zero

modified theorem ModularGroup.g_eq_of_c_eq_one

modified theorem ModularGroup.smul_eq_lcRow0_add

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

modified def CongruenceSubgroup.Gamma0

deleted theorem CongruenceSubgroup.Gamma0_det

modified theorem CongruenceSubgroup.Gamma0_mem

modified theorem CongruenceSubgroup.Gamma1_mem'

modified theorem CongruenceSubgroup.Gamma1_to_Gamma0_mem

modified def CongruenceSubgroup.Gamma

modified theorem CongruenceSubgroup.Gamma_mem'

modified theorem CongruenceSubgroup.Gamma_mem

modified theorem CongruenceSubgroup.Gamma_normal

modified theorem SL_reduction_mod_hom_val

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

Modified Mathlib/NumberTheory/ModularForms/Identities.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean

deleted theorem ModularForm.mul_slash_subgroup

modified theorem ModularForm.slash_action_eq'_iff

deleted theorem ModularForm.subgroup_slash

Modified Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

deleted theorem SlashInvariantForm.SlashInvariantFormClass.coe_coe

modified theorem SlashInvariantForm.coe_mk

added theorem SlashInvariantForm.slash_action_eqn''

modified theorem SlashInvariantForm.slash_action_eqn'

modified theorem SlashInvariantForm.slash_action_eqn