Commit 2026-03-25 15:49 9cb78157

View on Github →

refactor(GroupTheory/Commutator/Basic): to_additivize commutators (#34784) This PR makes some progress on to_additivizing more of the group theory library. I had to make the bracket instance scoped to avoid clashing with the Lie bracket.

Estimated changes

Modified Mathlib/Algebra/Group/Commutator.lean

added def commutatorElement

Modified Mathlib/Algebra/Group/Conj.lean

modified theorem conj_inv

modified theorem conj_mul

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

Modified Mathlib/GroupTheory/Commutator/Basic.lean

modified theorem conjugate_commutatorElement

Modified Mathlib/GroupTheory/Focal.lean

modified theorem Subgroup.map_focalSubgroupOf

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean

Modified Mathlib/GroupTheory/Solvable.lean

Modified Mathlib/Tactic/Translate/ToAdditive.lean

Modified Mathlib/Topology/Algebra/Group/TopologicalAbelianization.lean

Modified MathlibTest/Group.lean

Modified MathlibTest/toAdditiveIrredDef.lean