Commit 2025-09-25 05:05 38dae6bb

View on Github →

feat(GroupTheory/Commensurable): additivize (#29707) Move Commensurable into the Subgroup namespace, and add to_additive flags (hence auto-creating a parallel def AddSubgroup.commensurable)

Estimated changes

Modified Mathlib/GroupTheory/Commensurable.lean

deleted theorem Commensurable.comm

deleted theorem Commensurable.commensurable_conj

deleted theorem Commensurable.commensurable_inv

deleted def Commensurable.commensurator'

deleted theorem Commensurable.commensurator'_mem_iff

deleted def Commensurable.commensurator

deleted theorem Commensurable.commensurator_mem_iff

deleted theorem Commensurable.eq

deleted theorem Commensurable.equivalence

deleted def Commensurable.quotConjEquiv

deleted theorem Commensurable.symm

deleted theorem Commensurable.trans

deleted def Commensurable

added theorem Subgroup.Commensurable.comm

added theorem Subgroup.Commensurable.commensurable_conj

added theorem Subgroup.Commensurable.commensurable_inv

added def Subgroup.Commensurable.commensurator'

added theorem Subgroup.Commensurable.commensurator'_mem_iff

added def Subgroup.Commensurable.commensurator

added theorem Subgroup.Commensurable.commensurator_mem_iff

added theorem Subgroup.Commensurable.conj

added theorem Subgroup.Commensurable.eq

added theorem Subgroup.Commensurable.equivalence

added theorem Subgroup.Commensurable.symm

added theorem Subgroup.Commensurable.trans

added def Subgroup.Commensurable

added def Subgroup.quotConjEquiv

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

deleted theorem CongruenceSubgroup.IsArithmetic.conj

added theorem Subgroup.IsArithmetic.conj

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

deleted theorem Commensurable.isCusp_iff

added theorem Subgroup.Commensurable.isCusp_iff