Theorem Abelianization.commutator_subset_ker

Modification history

2026-10-17 13:25
Mathlib/GroupTheory/Abelianization/Defs.lean
chore(GroupTheory/Solvable): to_additivize file (#43108) …
Deleted Abelianization.commutator_subset_kerView on Github →
2025-07-23 15:29
Mathlib/GroupTheory/Abelianization.lean
chore(GroupTheory/FreeAbelianGroup): do not import cardinals (#27169) …
Modified Abelianization.commutator_subset_kerView on Github →
2023-02-11 21:40
Mathlib/GroupTheory/Abelianization.lean
feat: port GroupTheory.Abelianization (#2215)
Added Abelianization.commutator_subset_kerView on Github →