Commit 2025-11-28 11:46 d19e7691

View on Github →

feat(NumberTheory/ModularForms): adjoin -1 to a subgroup (#30649) Given a subgroup of GL(2, R), form the subgroup generated by it and -1. Using this, define the width of a subgroup.

Estimated changes

Modified Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean

added def Subgroup.adjoinNegOne

added theorem Subgroup.adjoinNegOne_eq_self_iff

added theorem Subgroup.commensurable_adjoinNegOne_self

added theorem Subgroup.hasDetOne_adjoinNegOne_iff

added theorem Subgroup.hasDetPlusMinusOne_adjoinNegOne_iff

added theorem Subgroup.le_adjoinNegOne

added theorem Subgroup.mem_adjoinNegOne_iff

added theorem Subgroup.negOne_mem_adjoinNegOne

added theorem Subgroup.relIndex_adjoinNegOne_ne_zero

added theorem Subgroup.relindex_adjoinNegOne_eq_two

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

added theorem Subgroup.IsRegularAtInfty.eq

added def Subgroup.IsRegularAtInfty

added theorem Subgroup.commensurable_strictPeriods_periods

added theorem Subgroup.isRegularAtInfty_iff

added theorem Subgroup.isRegularAtInfty_of_neg_one_mem

added theorem Subgroup.periods_eq_zmultiples_widthInfty

added theorem Subgroup.relIndex_strictPeriods

added theorem Subgroup.strictPeriods_eq_periods_of_neg_one_mem

added theorem Subgroup.strictPeriods_le_periods

added theorem Subgroup.two_mul_withInfty_mem_strictPeriods

added theorem Subgroup.widthInfty_mem_periods

added theorem Subgroup.widthInfty_nonneg

added theorem Subgroup.widthInfty_pos

added theorem Subgroup.widthInfty_pos_iff