Theorem map_commutator_eq

Modification history

2025-07-23 15:29

Mathlib/GroupTheory/Abelianization.lean

chore(GroupTheory/FreeAbelianGroup): do not import cardinals (#27169) …

Modified map_commutator_eq View on Github →

2025-02-07 14:21

Mathlib/GroupTheory/Abelianization.lean

feat(GroupTheory/GroupAction/Iwasawa): the Iwasawa criterion for simplicity (#12048) …

Added map_commutator_eq View on Github →