Commit 2026-10-12 12:32 1ce668c1

View on Github →

chore(GroupTheory/Commutator/Basic): golf some proofs (#44193) This PR golfs a few long proofs in GroupTheory/Commutator/Basic.lean.

Estimated changes

Modified Mathlib/Algebra/Group/Hom/Defs.lean

Modified Mathlib/GroupTheory/Commutator/Basic.lean

modified theorem map_commutator_eq

added theorem map_commutator_of_surjective

Modified Mathlib/GroupTheory/GroupAction/Iwasawa.lean