Commit 2024-12-19 09:16 dac878dc

View on Github →

chore: move transferTransversal (#20042) The last section of GroupTheory.Complement is a mix of results purely about ZMod and results about the transfer transversal. The former can move to Data.ZMod.Quotient, while the latter can move to GroupTheory.Transfer.

Estimated changes

Modified Mathlib/Data/ZMod/Quotient.lean

added theorem Subgroup.quotientEquivSigmaZMod_apply

added theorem Subgroup.quotientEquivSigmaZMod_symm_apply

Modified Mathlib/GroupTheory/Complement.lean

deleted theorem Subgroup.coe_transferFunction

deleted theorem Subgroup.mem_transferSet

deleted theorem Subgroup.quotientEquivSigmaZMod_apply

deleted theorem Subgroup.quotientEquivSigmaZMod_symm_apply

deleted theorem Subgroup.transferFunction_apply

deleted def Subgroup.transferSet

deleted def Subgroup.transferTransversal

deleted theorem Subgroup.transferTransversal_apply''

deleted theorem Subgroup.transferTransversal_apply'

deleted theorem Subgroup.transferTransversal_apply

Modified Mathlib/GroupTheory/CosetCover.lean

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.inf_eq_bot_of_coprime

Modified Mathlib/GroupTheory/OrderOfElement.lean

deleted theorem inf_eq_bot_of_coprime

Modified Mathlib/GroupTheory/Transfer.lean

added theorem Subgroup.coe_transferFunction

added theorem Subgroup.mem_transferSet

added theorem Subgroup.transferFunction_apply

added def Subgroup.transferSet

added def Subgroup.transferTransversal

added theorem Subgroup.transferTransversal_apply''

added theorem Subgroup.transferTransversal_apply'

added theorem Subgroup.transferTransversal_apply