Commit 2023-02-11 15:32 8e9c3b9a

View on Github →

feat: port GroupTheory.Commutator (#2143)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Commutator.lean

added theorem Commute.commutator_eq

added theorem Subgroup.commutator_bot_left

added theorem Subgroup.commutator_bot_right

added theorem Subgroup.commutator_comm

added theorem Subgroup.commutator_comm_le

added theorem Subgroup.commutator_commutator_eq_bot_of_rotate

added theorem Subgroup.commutator_def'

added theorem Subgroup.commutator_def

added theorem Subgroup.commutator_eq_bot_iff_le_centralizer

added theorem Subgroup.commutator_le

added theorem Subgroup.commutator_le_inf

added theorem Subgroup.commutator_le_left

added theorem Subgroup.commutator_le_map_commutator

added theorem Subgroup.commutator_le_right

added theorem Subgroup.commutator_mem_commutator

added theorem Subgroup.commutator_mono

added theorem Subgroup.commutator_pi_pi_le

added theorem Subgroup.commutator_pi_pi_of_finite

added theorem Subgroup.commutator_prod_prod

added theorem Subgroup.map_commutator

added theorem commutatorElement_eq_one_iff_commute

added theorem commutatorElement_eq_one_iff_mul_comm

added theorem commutatorElement_inv

added theorem commutatorElement_one_left

added theorem commutatorElement_one_right

added theorem commutatorElement_self

added def commutatorSet

added theorem commutatorSet_def

added theorem commutator_mem_commutatorSet

added theorem conjugate_commutatorElement

added theorem map_commutatorElement

added theorem mem_commutatorSet_iff

added theorem one_mem_commutatorSet