Commit 2022-11-01 18:20 bdfa72be

View on Github →

feat(group_theory/commutator): Define the set of commutators (#17276) With some of my upcoming group theory PRs, it is going to start being helpful to have a name for the set of commutators.

Estimated changes

Modified src/group_theory/abelianization.lean

modified theorem commutator_eq_closure

modified theorem rank_commutator_le_card

Modified src/group_theory/commutator.lean

added theorem commutator_mem_commutator_set

added def commutator_set

added theorem commutator_set_def

added theorem mem_commutator_set_iff

added theorem one_mem_commutator_set

Modified src/group_theory/schreier.lean

modified theorem subgroup.card_commutator_dvd_index_center_pow