Commit 2026-10-01 14:00 726a7f1e

View on Github →

chore(GroupTheory/Perm/*): switch from ConjAct to MulAut.conj (#44059) These results only need the conjugation map, not the full type synonym, so we can just MulAut.conj directly, allowing for some small golfs. This also allows us to clean up a few statements where some of the variables were in Perm and some were in ConjAct Perm. (I'll rename the file in a follow-up PR).

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Pointwise.lean

added theorem MulAut.coe_conj_apply

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

added theorem Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.conj_smul_mem_cycleFactorsFinset

deleted theorem Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset

Modified Mathlib/GroupTheory/Perm/ConjAct.lean

modified theorem Equiv.Perm.cycleFactorsFinset_conj_eq

modified theorem Equiv.Perm.mem_conj_support

modified theorem Equiv.Perm.mem_cycleFactorsFinset_conj'

modified theorem Equiv.Perm.support_conj_eq_smul_support

deleted theorem Equiv.Perm.support_toConjAct_eq_smul_support

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating/Simple.lean