Basic

📁 Source: Mathlib/GroupTheory/Commutator/Basic.lean

Statistics

Metric	Count
Definitions `addCommutator`, `commutator`, `addCommutator`, `addCommutatorRepresentatives`, `addCommutatorSet`, `closureAddCommutatorRepresentatives`, `closureCommutatorRepresentatives`, `commutator`, `commutatorRepresentatives`, `commutatorSet`, `instCharacteristicAddCommutator`, `instCharacteristicCommutator`, `instNormalAddCommutator`, `instNormalCommutator`	14
Theorems `addCommutator_eq`, `addCommutator_le_of_self_sup_commutative_eq_top`, `of_addCommutator_le`, `quotient_commutative_iff_addCommutator_le`, `addCommutator_addCommutator_eq_bot_of_rotate`, `addCommutator_bot_left`, `addCommutator_bot_right`, `addCommutator_characteristic`, `addCommutator_comm`, `addCommutator_comm_le`, `addCommutator_def`, `addCommutator_def'`, `addCommutator_eq_bot_iff_le_centralizer`, `addCommutator_le`, `addCommutator_le_inf`, `addCommutator_le_left`, `addCommutator_le_map_addCommutator`, `addCommutator_le_right`, `addCommutator_le_self`, `addCommutator_mem_addCommutator`, `addCommutator_mono`, `addCommutator_normal`, `addCommutator_pi_pi_le`, `addCommutator_sum_sum`, `addCommutator_top_left_le_iff`, `addCommutator_top_right_le_iff`, `map_addCommutator`, `map_subtype_addCommutator`, `commutator_eq`, `commutator_le_of_self_sup_commutative_eq_top`, `of_commutator_le`, `quotient_commutative_iff_commutator_le`, `commutator_bot_left`, `commutator_bot_right`, `commutator_characteristic`, `commutator_comm`, `commutator_comm_le`, `commutator_commutator_eq_bot_of_rotate`, `commutator_def`, `commutator_def'`, `commutator_eq_bot_iff_le_centralizer`, `commutator_le`, `commutator_le_inf`, `commutator_le_left`, `commutator_le_map_commutator`, `commutator_le_right`, `commutator_le_self`, `commutator_mem_commutator`, `commutator_mono`, `commutator_normal`, `commutator_pi_pi_le`, `commutator_prod_prod`, `commutator_top_left_le_iff`, `commutator_top_right_le_iff`, `map_commutator`, `map_subtype_commutator`, `addCommutatorElement_eq_zero_iff_addCommute`, `addCommutatorElement_eq_zero_iff_add_comm`, `addCommutatorElement_neg`, `addCommutatorElement_self`, `addCommutatorElement_zero_left`, `addCommutatorElement_zero_right`, `addCommutatorSet_def`, `addCommutator_centralizer_addCommutator_le_center`, `addCommutator_def`, `addCommutator_eq_bot_iff_center_eq_top`, `addCommutator_eq_closure`, `addCommutator_eq_normalClosure`, `addCommutator_mem_addCommutatorSet`, `commutatorElement_eq_one_iff_commute`, `commutatorElement_eq_one_iff_mul_comm`, `commutatorElement_inv`, `commutatorElement_one_left`, `commutatorElement_one_right`, `commutatorElement_self`, `commutatorSet_def`, `commutator_centralizer_commutator_le_center`, `commutator_def`, `commutator_eq_bot_iff_center_eq_top`, `commutator_eq_closure`, `commutator_eq_normalClosure`, `commutator_mem_commutatorSet`, `conjugate_addCommutatorElement`, `conjugate_commutatorElement`, `image_addCommutatorSet_closureAddCommutatorRepresentatives`, `image_commutatorSet_closureCommutatorRepresentatives`, `instNonemptyElemAddCommutatorSet`, `instNonemptyElemCommutatorSet`, `map_addCommutatorElement`, `map_addCommutator_eq`, `map_commutatorElement`, `map_commutator_eq`, `mem_addCommutatorSet_iff`, `mem_addCommutatorSet_of_isAddConj_sq`, `mem_commutatorSet_iff`, `mem_commutatorSet_of_isConj_sq`, `one_mem_commutatorSet`, `zero_mem_addCommutatorSet`	98
Total	112

AddCommute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommutator_eq` 📖	mathematical	`AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`Bracket.bracket` `addCommutatorElement` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`addCommutatorElement_eq_zero_iff_addCommute`

AddSubgroup

Definitions

Name	Category	Theorems
`addCommutator` 📖	CompOp	28 math math: `addCommutator_comm_le`, `addCommutator_top_left_le_iff`, `addCommutator_pi_pi_le`, `addCommutator_comm`, `addCommutator_mem_addCommutator`, `addCommutator_def`, `addCommutator_sum_sum`, `addCommutator_bot_left`, `addCommutator_le`, `addCommutator_top_right_le_iff`, `addCommutator_centralizer_addCommutator_le_center`, `addCommutator_bot_right`, `map_subtype_addCommutator`, `addCommutator_le_map_addCommutator`, `addCommutator_le_right`, `addCommutator_le_left`, `map_addCommutator_eq`, `addCommutator_def`, `addCommutator_le_focalAddSubgroup`, `addCommutator_addCommutator_eq_bot_of_rotate`, `addCommutator_def'`, `map_addCommutator`, `addCommutator_le_inf`, `addCommutator_mono`, `addCommutator_characteristic`, `addCommutator_le_self`, `addCommutator_normal`, `addCommutator_eq_bot_iff_le_centralizer`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommutator_addCommutator_eq_bot_of_rotate` 📖	mathematical	`Bracket.bracket` `AddSubgroup` `addCommutator` `Bot.bot` `instBot`	`Bracket.bracket` `AddSubgroup` `addCommutator` `Bot.bot` `instBot`	—	`addCommutator_eq_bot_iff_le_centralizer` `addCommutator_le` `mem_centralizer_iff_addCommutator_eq_zero` `add_assoc` `neg_add_rev` `neg_neg` `add_neg_cancel_left` `neg_add_cancel_left` `neg_mem` `neg_zero` `add_zero` `add_neg_cancel`
`addCommutator_bot_left` 📖	mathematical	—	`Bracket.bracket` `AddSubgroup` `addCommutator` `Bot.bot` `instBot`	—	`le_bot_iff` `addCommutator_le_left` `normal_bot`
`addCommutator_bot_right` 📖	mathematical	—	`Bracket.bracket` `AddSubgroup` `addCommutator` `Bot.bot` `instBot`	—	`le_bot_iff` `addCommutator_le_right` `normal_bot`
`addCommutator_characteristic` 📖	mathematical	—	`Characteristic` `Bracket.bracket` `AddSubgroup` `addCommutator`	—	`characteristic_iff_le_map` `addCommutator_le_map_addCommutator`
`addCommutator_comm` 📖	mathematical	—	`Bracket.bracket` `AddSubgroup` `addCommutator`	—	`le_antisymm` `addCommutator_comm_le`
`addCommutator_comm_le` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator`	—	`addCommutator_le` `neg_mem_iff` `addCommutator_mem_addCommutator` `addCommutatorElement_neg`
`addCommutator_def` 📖	mathematical	—	`Bracket.bracket` `AddSubgroup` `addCommutator` `closure` `setOf` `SetLike.instMembership` `instSetLike` `addCommutatorElement`	—	—
`addCommutator_def'` 📖	mathematical	—	`Bracket.bracket` `AddSubgroup` `addCommutator` `normalClosure` `setOf` `SetLike.instMembership` `instSetLike` `addCommutatorElement`	—	`le_antisymm` `closure_le_normalClosure` `normalClosure_le_normal` `addCommutator_normal` `subset_closure`
`addCommutator_eq_bot_iff_le_centralizer` 📖	mathematical	—	`Bracket.bracket` `AddSubgroup` `addCommutator` `Bot.bot` `instBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer` `SetLike.coe` `instSetLike`	—	`eq_bot_iff` `addCommutator_le` `mem_bot` `addCommutatorElement_eq_zero_iff_add_comm`
`addCommutator_le` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator` `SetLike.instMembership` `instSetLike` `addCommutatorElement`	—	`closure_le`
`addCommutator_le_inf` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator` `instMin`	—	`le_inf` `addCommutator_le_left` `addCommutator_le_right`
`addCommutator_le_left` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator`	—	`addCommutator_le_right` `addCommutator_comm`
`addCommutator_le_map_addCommutator` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map`	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator` `map`	—	`LE.le.trans` `addCommutator_mono` `ge_of_eq` `map_addCommutator`
`addCommutator_le_right` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator`	—	`addCommutator_le` `add_mem` `Normal.conj_mem` `neg_mem`
`addCommutator_le_self` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator`	—	`Eq.trans_le` `map_subtype_addCommutator` `map_subtype_le`
`addCommutator_mem_addCommutator` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `instSetLike`	`AddSubgroup` `SetLike.instMembership` `instSetLike` `Bracket.bracket` `addCommutator` `addCommutatorElement`	—	`subset_closure`
`addCommutator_mono` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator`	—	`addCommutator_le` `addCommutator_mem_addCommutator`
`addCommutator_normal` 📖	mathematical	—	`Normal` `Bracket.bracket` `AddSubgroup` `addCommutator`	—	`Set.Subset.antisymm` `AddGroup.subset_addConjugatesOfSet` `isAddConj_iff` `AddGroup.mem_addConjugatesOfSet_iff` `Normal.conj_mem` `conjugate_addCommutatorElement` `normalClosure_normal`
`addCommutator_pi_pi_le` 📖	mathematical	—	`AddSubgroup` `Pi.addGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator` `pi` `Set.univ`	—	`addCommutator_le` `addCommutator_mem_addCommutator`
`addCommutator_sum_sum` 📖	mathematical	—	`Bracket.bracket` `AddSubgroup` `Prod.instAddGroup` `addCommutator` `prod`	—	`le_antisymm` `addCommutator_le` `addCommutator_mem_addCommutator` `prod_le_iff` `map_addCommutator` `addCommutator_mono` `le_prod_iff` `map_map` `map_id` `instReflLe` `map_zero_eq_bot` `bot_le`
`addCommutator_top_left_le_iff` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator` `Top.top` `instTop` `Normal`	—	`add_mem_cancel_right` `neg_mem` `addCommutator_le` `addCommutator_le_right`
`addCommutator_top_right_le_iff` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `addCommutator` `Top.top` `instTop` `Normal`	—	`addCommutator_top_left_le_iff` `addCommutator_comm`
`map_addCommutator` 📖	mathematical	—	`map` `Bracket.bracket` `AddSubgroup` `addCommutator`	—	`le_antisymm_iff` `map_le_iff_le_comap` `addCommutator_le` `mem_comap` `map_addCommutatorElement` `AddMonoidHom.instAddMonoidHomClass` `addCommutator_mem_addCommutator` `mem_map_of_mem`
`map_subtype_addCommutator` 📖	mathematical	—	`map` `AddSubgroup` `SetLike.instMembership` `instSetLike` `toAddGroup` `subtype` `addCommutator` `Bracket.bracket` `addCommutator`	—	`addCommutator_def` `map_addCommutator` `AddMonoidHom.range_eq_map` `range_subtype`

AddSubgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommutator_le_of_self_sup_commutative_eq_top` 📖	mathematical	`AddSubgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AddSubgroup.instCompleteLattice` `Top.top` `AddSubgroup.instTop`	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `addCommutator`	—	`quotient_commutative_iff_addCommutator_le` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Function.Surjective.add_comm` `AddHom.coe_coe` `AddMonoidHom.range_eq_top` `AddMonoidHom.range_eq_map` `AddSubgroup.map_map` `QuotientAddGroup.mk'_surjective` `AddSubgroup.map_eq_map_iff` `QuotientAddGroup.ker_mk'` `sup_comm` `AddSubgroup.range_subtype` `sup_of_le_right` `le_sup_left` `IsAddCommutative.is_comm`
`of_addCommutator_le` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `addCommutator`	`AddSubgroup.Normal`	—	`AddSubgroup.addCommutator_top_left_le_iff` `LE.le.trans` `AddSubgroup.addCommutator_mono` `le_top`
`quotient_commutative_iff_addCommutator_le` 📖	mathematical	—	`HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `addCommutator`	—	`addCommutator_eq_normalClosure` `AddSubgroup.normalClosure_subset_iff` `SetLike.mem_coe` `QuotientAddGroup.eq_zero_iff` `addCommutatorElement_def` `addCommutatorElement_eq_zero_iff_add_comm` `QuotientAddGroup.mk'_surjective` `map_addCommutatorElement` `AddMonoidHom.instAddMonoidHomClass` `QuotientAddGroup.mk'_apply` `addCommutator_eq_closure` `AddSubgroup.subset_closure` `addCommutator_mem_addCommutatorSet`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_eq` 📖	mathematical	`Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`Bracket.bracket` `commutatorElement` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`commutatorElement_eq_one_iff_commute`

Subgroup

Definitions

Name	Category	Theorems
`commutator` 📖	CompOp	37 math math: `IsSolvable.commutator_lt_of_ne_bot`, `commutator_def'`, `commutator_mono`, `commutator_le_right`, `commutator_prod_prod`, `derivedSeries_succ`, `commutator_commutator_eq_bot_of_rotate`, `commutator_le`, `commutator_eq_self`, `map_commutator_eq`, `commutator_comm`, `commutator_pi_pi_le`, `commutator_le_self`, `commutator_eq_bot_iff_le_centralizer`, `Sylow.commutator_eq_bot_or_commutator_eq_self`, `commutator_bot_right`, `commutator_mem_commutator`, `IsPGroup.commutator_eq_bot_or_commutator_eq_self`, `commutator_def`, `isPerfect_iff`, `commutator_le_inf`, `commutator_top_right_le_iff`, `commutator_le_focalSubgroup`, `commutator_centralizer_commutator_le_center`, `commutator_top_left_le_iff`, `commutator_le_map_commutator`, `isSolvable_iff_commutator_lt`, `commutator_def`, `commutator_comm_le`, `map_commutator`, `commutator_le_left`, `commutator_characteristic`, `commutator_alternatingGroup_eq_self`, `commutator_bot_left`, `commutator_pi_pi_of_finite`, `commutator_normal`, `map_subtype_commutator`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_bot_left` 📖	mathematical	—	`Bracket.bracket` `Subgroup` `commutator` `Bot.bot` `instBot`	—	`le_bot_iff` `commutator_le_left` `normal_bot`
`commutator_bot_right` 📖	mathematical	—	`Bracket.bracket` `Subgroup` `commutator` `Bot.bot` `instBot`	—	`le_bot_iff` `commutator_le_right` `normal_bot`
`commutator_characteristic` 📖	mathematical	—	`Characteristic` `Bracket.bracket` `Subgroup` `commutator`	—	`characteristic_iff_le_map` `commutator_le_map_commutator`
`commutator_comm` 📖	mathematical	—	`Bracket.bracket` `Subgroup` `commutator`	—	`le_antisymm` `commutator_comm_le`
`commutator_comm_le` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator`	—	`commutator_le` `inv_mem_iff` `commutator_mem_commutator` `commutatorElement_inv`
`commutator_commutator_eq_bot_of_rotate` 📖	mathematical	`Bracket.bracket` `Subgroup` `commutator` `Bot.bot` `instBot`	`Bracket.bracket` `Subgroup` `commutator` `Bot.bot` `instBot`	—	`mul_assoc` `mul_inv_rev` `inv_inv` `mul_inv_cancel_left` `inv_mul_cancel_left` `inv_mem` `inv_one` `mul_one` `mul_inv_cancel`
`commutator_def` 📖	mathematical	—	`Bracket.bracket` `Subgroup` `commutator` `closure` `setOf` `SetLike.instMembership` `instSetLike` `commutatorElement`	—	—
`commutator_def'` 📖	mathematical	—	`Bracket.bracket` `Subgroup` `commutator` `normalClosure` `setOf` `SetLike.instMembership` `instSetLike` `commutatorElement`	—	`le_antisymm` `closure_le_normalClosure` `normalClosure_le_normal` `commutator_normal` `subset_closure`
`commutator_eq_bot_iff_le_centralizer` 📖	mathematical	—	`Bracket.bracket` `Subgroup` `commutator` `Bot.bot` `instBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer` `SetLike.coe` `instSetLike`	—	`eq_bot_iff` `commutator_le` `mem_bot` `commutatorElement_eq_one_iff_mul_comm`
`commutator_le` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator` `SetLike.instMembership` `instSetLike` `commutatorElement`	—	`closure_le`
`commutator_le_inf` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator` `instMin`	—	`le_inf` `commutator_le_left` `commutator_le_right`
`commutator_le_left` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator`	—	`commutator_le_right` `commutator_comm`
`commutator_le_map_commutator` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map`	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator` `map`	—	`LE.le.trans` `commutator_mono` `ge_of_eq` `map_commutator`
`commutator_le_right` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator`	—	`commutator_le` `mul_mem` `Normal.conj_mem` `inv_mem`
`commutator_le_self` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator`	—	`Eq.trans_le` `map_subtype_commutator` `map_subtype_le`
`commutator_mem_commutator` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike`	`Subgroup` `SetLike.instMembership` `instSetLike` `Bracket.bracket` `commutator` `commutatorElement`	—	`subset_closure`
`commutator_mono` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator`	—	`commutator_le` `commutator_mem_commutator`
`commutator_normal` 📖	mathematical	—	`Normal` `Bracket.bracket` `Subgroup` `commutator`	—	`Set.Subset.antisymm` `Group.subset_conjugatesOfSet` `Normal.conj_mem` `conjugate_commutatorElement` `normalClosure_normal`
`commutator_pi_pi_le` 📖	mathematical	—	`Subgroup` `Pi.group` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator` `pi` `Set.univ`	—	`commutator_le` `commutator_mem_commutator`
`commutator_prod_prod` 📖	mathematical	—	`Bracket.bracket` `Subgroup` `Prod.instGroup` `commutator` `prod`	—	`le_antisymm` `commutator_le` `commutator_mem_commutator` `prod_le_iff` `map_commutator` `commutator_mono` `map_map` `map_id` `instReflLe` `map_one_eq_bot`
`commutator_top_left_le_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator` `Top.top` `instTop` `Normal`	—	`mul_mem_cancel_right` `inv_mem` `commutator_le` `commutator_le_right`
`commutator_top_right_le_iff` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `commutator` `Top.top` `instTop` `Normal`	—	`commutator_top_left_le_iff` `commutator_comm`
`map_commutator` 📖	mathematical	—	`map` `Bracket.bracket` `Subgroup` `commutator`	—	`map_commutatorElement` `MonoidHom.instMonoidHomClass` `commutator_mem_commutator` `mem_map_of_mem`
`map_subtype_commutator` 📖	mathematical	—	`map` `Subgroup` `SetLike.instMembership` `instSetLike` `toGroup` `subtype` `commutator` `Bracket.bracket` `commutator`	—	`commutator_def` `map_commutator` `MonoidHom.range_eq_map` `range_subtype`

Subgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_le_of_self_sup_commutative_eq_top` 📖	mathematical	`Subgroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Subgroup.instCompleteLattice` `Top.top` `Subgroup.instTop`	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `commutator`	—	`quotient_commutative_iff_commutator_le` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Function.Surjective.mul_comm` `MulHom.coe_coe` `MonoidHom.range_eq_top` `MonoidHom.range_eq_map` `QuotientGroup.mk'_surjective` `QuotientGroup.ker_mk'` `sup_comm` `Subgroup.range_subtype` `sup_of_le_right` `IsMulCommutative.is_comm`
`of_commutator_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `commutator`	`Subgroup.Normal`	—	`Subgroup.commutator_top_left_le_iff` `LE.le.trans` `Subgroup.commutator_mono` `le_top`
`quotient_commutative_iff_commutator_le` 📖	mathematical	—	`HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `commutator`	—	`commutator_eq_normalClosure` `Subgroup.normalClosure_subset_iff` `SetLike.mem_coe` `QuotientGroup.eq_one_iff` `commutatorElement_def` `QuotientGroup.mk'_surjective` `commutatorElement_eq_one_iff_mul_comm` `map_commutatorElement` `MonoidHom.instMonoidHomClass` `QuotientGroup.mk'_apply` `commutator_eq_closure` `Subgroup.subset_closure` `commutator_mem_commutatorSet`

(root)

Definitions

Name	Category	Theorems
`addCommutator` 📖	CompOp	11 math math: `AddSubgroup.Normal.quotient_commutative_iff_addCommutator_le`, `AddSubgroup.addCommutator_le_focalAddSubgroupOf`, `addCommutator_eq_normalClosure`, `addCommutator_centralizer_addCommutator_le_center`, `AddSubgroup.map_subtype_addCommutator`, `addCommutator_eq_bot_iff_center_eq_top`, `AddSubgroup.Normal.addCommutator_le_of_self_sup_commutative_eq_top`, `map_addCommutator_eq`, `addCommutator_def`, `AddSubgroup.focalAddSubgroup_le_addCommutator`, `addCommutator_eq_closure`
`addCommutatorRepresentatives` 📖	CompOp	—
`addCommutatorSet` 📖	CompOp	9 math math: `addCommutatorSet_def`, `image_addCommutatorSet_closureAddCommutatorRepresentatives`, `addCommutator_eq_normalClosure`, `mem_addCommutatorSet_of_isAddConj_sq`, `zero_mem_addCommutatorSet`, `addCommutator_mem_addCommutatorSet`, `mem_addCommutatorSet_iff`, `instNonemptyElemAddCommutatorSet`, `addCommutator_eq_closure`
`closureAddCommutatorRepresentatives` 📖	CompOp	1 math math: `image_addCommutatorSet_closureAddCommutatorRepresentatives`
`closureCommutatorRepresentatives` 📖	CompOp	6 math math: `card_commutatorSet_closureCommutatorRepresentatives`, `instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet`, `card_commutator_closureCommutatorRepresentatives`, `image_commutatorSet_closureCommutatorRepresentatives`, `rank_closureCommutatorRepresentatives_le`, `closureCommutatorRepresentatives_fg`
`commutator` 📖	CompOp	43 math math: `MulAction.IwasawaStructure.commutator_le`, `Group.IsPerfect.mem_commutator`, `alternatingGroup.commutator_perm_eq`, `IsZGroup.coprime_commutator_index`, `commutator_eq_normalClosure`, `Abelianization.mk_eq_of`, `Subgroup.Normal.quotient_commutative_iff_commutator_le`, `Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup`, `IsSolvable.commutator_lt_top_of_nontrivial`, `commutator_eq_closure`, `Group.isPerfect_def`, `instNormalCommutatorClosure`, `alternatingGroup.kleinFour_eq_commutator`, `Field.absoluteGaloisGroup.commutator_closure_isNormal`, `Subgroup.card_commutator_le_of_finite_commutatorSet`, `Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator`, `map_commutator_eq`, `Subgroup.rank_commutator_le_card`, `Sylow.normalizer_le_centralizer_or_le_commutator`, `Subgroup.instFiniteSubtypeMemCommutatorOfElemCommutatorSet`, `IsSimpleGroup.derivedSeries_succ`, `Subgroup.card_commutator_dvd_index_center_pow`, `Sylow.le_center_or_le_commutator`, `lowerCentralSeries_one`, `Group.IsPerfect.commutator_eq_top`, `IsZGroup.commutator_lt`, `commutator_centralizer_commutator_le_center`, `derivedSeries_one`, `commutator_alternatingGroup_eq_top`, `Subgroup.instFGSubtypeMemCommutator`, `Subgroup.commutator_inf_eq_focalSubgroup`, `Subgroup.focalSubgroup_le_commutator`, `card_commutator_closureCommutatorRepresentatives`, `Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top`, `alternatingGroup.commutator_perm_le`, `IsZGroup.isCyclic_commutator`, `Subgroup.commutator_le_focalSubgroupOf`, `commutator_def`, `Abelianization.ker_of`, `inv_card_commutator_le_commProb`, `commutator_eq_bot_iff_center_eq_top`, `Abelianization.commutator_subset_ker`, `Subgroup.map_subtype_commutator`
`commutatorRepresentatives` 📖	CompOp	1 math math: `instFiniteElemProdCommutatorRepresentatives`
`commutatorSet` 📖	CompOp	19 math math: `Subgroup.index_center_le_pow`, `one_mem_commutatorSet`, `commutator_eq_normalClosure`, `commutator_mem_commutatorSet`, `Subgroup.quotientCentralizerEmbedding_apply`, `mem_commutatorSet_of_isConj_sq`, `commutator_eq_closure`, `Subgroup.card_commutator_le_of_finite_commutatorSet`, `mem_commutatorSet_iff`, `card_commutatorSet_closureCommutatorRepresentatives`, `Subgroup.rank_commutator_le_card`, `Subgroup.card_commutator_dvd_index_center_pow`, `instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet`, `Subgroup.quotientCenterEmbedding_apply`, `Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup`, `instNonemptyElemCommutatorSet`, `commutatorSet_def`, `image_commutatorSet_closureCommutatorRepresentatives`, `rank_closureCommutatorRepresentatives_le`
`instCharacteristicAddCommutator` 📖	CompOp	—
`instCharacteristicCommutator` 📖	CompOp	—
`instNormalAddCommutator` 📖	CompOp	—
`instNormalCommutator` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCommutatorElement_eq_zero_iff_addCommute` 📖	mathematical	—	`Bracket.bracket` `addCommutatorElement` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`addCommutatorElement_eq_zero_iff_add_comm`
`addCommutatorElement_eq_zero_iff_add_comm` 📖	mathematical	—	`Bracket.bracket` `addCommutatorElement` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`addCommutatorElement_def` `add_neg_eq_zero` `add_neg_eq_iff_eq_add`
`addCommutatorElement_neg` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Bracket.bracket` `addCommutatorElement`	—	`neg_add_rev` `neg_neg` `add_assoc`
`addCommutatorElement_self` 📖	mathematical	—	`Bracket.bracket` `addCommutatorElement` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddCommute.addCommutator_eq` `AddCommute.refl`
`addCommutatorElement_zero_left` 📖	mathematical	—	`Bracket.bracket` `addCommutatorElement` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddCommute.addCommutator_eq` `AddCommute.zero_left`
`addCommutatorElement_zero_right` 📖	mathematical	—	`Bracket.bracket` `addCommutatorElement` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddCommute.addCommutator_eq` `AddCommute.zero_right`
`addCommutatorSet_def` 📖	mathematical	—	`addCommutatorSet` `setOf` `Bracket.bracket` `addCommutatorElement`	—	—
`addCommutator_centralizer_addCommutator_le_center` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `Bracket.bracket` `AddSubgroup.addCommutator` `AddSubgroup.centralizer` `SetLike.coe` `AddSubgroup.instSetLike` `addCommutator` `AddSubgroup.center`	—	`AddSubgroup.centralizer_univ` `AddSubgroup.coe_top` `AddSubgroup.addCommutator_eq_bot_iff_le_centralizer` `AddSubgroup.addCommutator_comm` `Set.addCentralizer_subset` `AddSubgroup.addCommutator_mono` `le_top` `AddSubgroup.addCommutator_addCommutator_eq_bot_of_rotate`
`addCommutator_def` 📖	mathematical	—	`addCommutator` `Bracket.bracket` `AddSubgroup` `AddSubgroup.addCommutator` `Top.top` `AddSubgroup.instTop`	—	—
`addCommutator_eq_bot_iff_center_eq_top` 📖	mathematical	—	`addCommutator` `Bot.bot` `AddSubgroup` `AddSubgroup.instBot` `AddSubgroup.center` `Top.top` `AddSubgroup.instTop`	—	`AddSubgroup.addCommutator_eq_bot_iff_le_centralizer` `top_le_iff` `AddSubgroup.centralizer_eq_top_iff_subset` `Set.univ_subset_iff` `AddSubgroup.coe_eq_univ`
`addCommutator_eq_closure` 📖	mathematical	—	`addCommutator` `AddSubgroup.closure` `addCommutatorSet`	—	`AddSubgroup.mem_top`
`addCommutator_eq_normalClosure` 📖	mathematical	—	`addCommutator` `AddSubgroup.normalClosure` `addCommutatorSet`	—	`AddSubgroup.addCommutator_def'` `AddSubgroup.normal_top` `AddSubgroup.mem_top`
`addCommutator_mem_addCommutatorSet` 📖	mathematical	—	`Set` `Set.instMembership` `addCommutatorSet` `Bracket.bracket` `addCommutatorElement`	—	—
`commutatorElement_eq_one_iff_commute` 📖	mathematical	—	`Bracket.bracket` `commutatorElement` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`commutatorElement_eq_one_iff_mul_comm`
`commutatorElement_eq_one_iff_mul_comm` 📖	mathematical	—	`Bracket.bracket` `commutatorElement` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`commutatorElement_def` `mul_inv_eq_one` `mul_inv_eq_iff_eq_mul`
`commutatorElement_inv` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Bracket.bracket` `commutatorElement`	—	`mul_inv_rev` `inv_inv` `mul_assoc`
`commutatorElement_one_left` 📖	mathematical	—	`Bracket.bracket` `commutatorElement` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Commute.commutator_eq` `Commute.one_left`
`commutatorElement_one_right` 📖	mathematical	—	`Bracket.bracket` `commutatorElement` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Commute.commutator_eq` `Commute.one_right`
`commutatorElement_self` 📖	mathematical	—	`Bracket.bracket` `commutatorElement` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Commute.commutator_eq` `Commute.refl`
`commutatorSet_def` 📖	mathematical	—	`commutatorSet` `setOf` `Bracket.bracket` `commutatorElement`	—	—
`commutator_centralizer_commutator_le_center` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Bracket.bracket` `Subgroup.commutator` `Subgroup.centralizer` `SetLike.coe` `Subgroup.instSetLike` `commutator` `Subgroup.center`	—	`Subgroup.centralizer_univ` `Subgroup.coe_top` `Subgroup.commutator_eq_bot_iff_le_centralizer` `Subgroup.commutator_comm` `Set.centralizer_subset` `Subgroup.commutator_mono` `le_top` `Subgroup.commutator_commutator_eq_bot_of_rotate`
`commutator_def` 📖	mathematical	—	`commutator` `Bracket.bracket` `Subgroup` `Subgroup.commutator` `Top.top` `Subgroup.instTop`	—	—
`commutator_eq_bot_iff_center_eq_top` 📖	mathematical	—	`commutator` `Bot.bot` `Subgroup` `Subgroup.instBot` `Subgroup.center` `Top.top` `Subgroup.instTop`	—	—
`commutator_eq_closure` 📖	mathematical	—	`commutator` `Subgroup.closure` `commutatorSet`	—	—
`commutator_eq_normalClosure` 📖	mathematical	—	`commutator` `Subgroup.normalClosure` `commutatorSet`	—	`Subgroup.commutator_def'` `Subgroup.normal_top`
`commutator_mem_commutatorSet` 📖	mathematical	—	`Set` `Set.instMembership` `commutatorSet` `Bracket.bracket` `commutatorElement`	—	—
`conjugate_addCommutatorElement` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Bracket.bracket` `addCommutatorElement` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`add_assoc` `neg_add_cancel_left` `neg_add_rev` `neg_neg`
`conjugate_commutatorElement` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Bracket.bracket` `commutatorElement` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_assoc` `inv_mul_cancel_left` `mul_inv_rev` `inv_inv`
`image_addCommutatorSet_closureAddCommutatorRepresentatives` 📖	mathematical	—	`Set.image` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `closureAddCommutatorRepresentatives` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddMonoidHom.instFunLike` `AddSubgroup.subtype` `addCommutatorSet`	—	`Set.Subset.antisymm` `AddSubgroup.subset_closure`
`image_commutatorSet_closureCommutatorRepresentatives` 📖	mathematical	—	`Set.image` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `closureCommutatorRepresentatives` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `Subgroup.subtype` `commutatorSet`	—	`Set.Subset.antisymm` `Subgroup.subset_closure`
`instNonemptyElemAddCommutatorSet` 📖	mathematical	—	`Set.Elem` `addCommutatorSet`	—	`zero_mem_addCommutatorSet`
`instNonemptyElemCommutatorSet` 📖	mathematical	—	`Set.Elem` `commutatorSet`	—	`one_mem_commutatorSet`
`map_addCommutatorElement` 📖	mathematical	—	`DFunLike.coe` `Bracket.bracket` `addCommutatorElement`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `map_neg`
`map_addCommutator_eq` 📖	mathematical	—	`AddSubgroup.map` `addCommutator` `Bracket.bracket` `AddSubgroup` `AddSubgroup.addCommutator` `AddMonoidHom.range`	—	`addCommutator_def` `AddSubgroup.map_addCommutator` `AddSubgroup.map_eq_range_iff` `codisjoint_iff` `top_sup_eq`
`map_commutatorElement` 📖	mathematical	—	`DFunLike.coe` `Bracket.bracket` `commutatorElement`	—	`map_mul` `MonoidHomClass.toMulHomClass` `map_inv`
`map_commutator_eq` 📖	mathematical	—	`Subgroup.map` `commutator` `Bracket.bracket` `Subgroup` `Subgroup.commutator` `MonoidHom.range`	—	`commutator_def` `Subgroup.map_commutator` `Subgroup.map_eq_range_iff` `codisjoint_iff` `top_sup_eq`
`mem_addCommutatorSet_iff` 📖	mathematical	—	`Set` `Set.instMembership` `addCommutatorSet` `Bracket.bracket` `addCommutatorElement`	—	—
`mem_addCommutatorSet_of_isAddConj_sq` 📖	mathematical	`IsAddConj` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoid.toNSMul`	`Set` `Set.instMembership` `addCommutatorSet`	—	`addCommutatorElement_def` `two_nsmul` `IsAddUnit.add_neg_cancel_right` `AddUnits.isAddUnit` `add_neg_eq_iff_eq_add`
`mem_commutatorSet_iff` 📖	mathematical	—	`Set` `Set.instMembership` `commutatorSet` `Bracket.bracket` `commutatorElement`	—	—
`mem_commutatorSet_of_isConj_sq` 📖	mathematical	`IsConj` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toPow`	`Set` `Set.instMembership` `commutatorSet`	—	`commutatorElement_def` `pow_two` `IsUnit.mul_inv_cancel_right`
`one_mem_commutatorSet` 📖	mathematical	—	`Set` `Set.instMembership` `commutatorSet` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`commutatorElement_self`
`zero_mem_addCommutatorSet` 📖	mathematical	—	`Set` `Set.instMembership` `addCommutatorSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`addCommutatorElement_self`

---

← Back to Index