Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 19:48 3da03b97

View on Github →

refactor(group_theory/commutator): Use variables and rearrange lemmas (#12629) This PR adds variables, and rearranges some of the lemmas (moving the lemmas about normal subgroups to a separate section).

Estimated changes

Modified src/group_theory/commutator.lean

modified theorem subgroup.commutator_bot_left

modified theorem subgroup.commutator_bot_right

modified theorem subgroup.commutator_comm

modified theorem subgroup.commutator_comm_le

modified theorem subgroup.commutator_def'

modified theorem subgroup.commutator_eq_bot_iff_le_centralizer

modified theorem subgroup.commutator_le

modified theorem subgroup.commutator_le_inf

modified theorem subgroup.commutator_le_left

modified theorem subgroup.commutator_le_right

modified theorem subgroup.commutator_mem_commutator

modified theorem subgroup.commutator_mono

modified theorem subgroup.commutator_prod_prod

modified theorem subgroup.map_commutator