Basic

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

Statistics

Metric	Count
Definitions commutator, closureCommutatorRepresentatives, commutator, commutatorRepresentatives, commutatorSet, instCharacteristicCommutator, instNormalCommutator	7
Theorems commutator_eq, commutator_le_of_self_sup_commutative_eq_top, 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, map_commutator, map_subtype_commutator, 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_commutatorElement, image_commutatorSet_closureCommutatorRepresentatives, instNonemptyElemCommutatorSet, map_commutatorElement, map_commutator_eq, mem_commutatorSet_iff, mem_commutatorSet_of_isConj_sq, one_mem_commutatorSet	46
Total	53

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	31 math math: IsSolvable.commutator_lt_of_ne_bot, commutator_def', commutator_mono, commutator_le_right, commutator_prod_prod, derivedSeries_succ, commutator_le, 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, commutator_le_inf, commutator_centralizer_commutator_le_center, 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 📖	—	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	Bracket.bracket commutator	—	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	Bracket.bracket commutator commutatorElement	—	subset_closure
commutator_mono 📖	mathematical	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 map_one_eq_bot
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	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
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
closureCommutatorRepresentatives 📖	CompOp	6 math math: card_commutatorSet_closureCommutatorRepresentatives, instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet, card_commutator_closureCommutatorRepresentatives, image_commutatorSet_closureCommutatorRepresentatives, rank_closureCommutatorRepresentatives_le, closureCommutatorRepresentatives_fg
commutator 📖	CompOp	37 math math: MulAction.IwasawaStructure.commutator_le, 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, 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, IsZGroup.commutator_lt, commutator_centralizer_commutator_le_center, derivedSeries_one, commutator_alternatingGroup_eq_top, Subgroup.instFGSubtypeMemCommutator, card_commutator_closureCommutatorRepresentatives, Subgroup.Normal.commutator_le_of_self_sup_commutative_eq_top, alternatingGroup.commutator_perm_le, IsZGroup.isCyclic_commutator, 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
instCharacteristicCommutator 📖	CompOp	—
instNormalCommutator 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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_commutatorElement 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Bracket.bracket commutatorElement InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	map_commutatorElement MonoidHom.instMonoidHomClass
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
instNonemptyElemCommutatorSet 📖	mathematical	—	Set.Elem commutatorSet	—	one_mem_commutatorSet
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_commutatorSet_iff 📖	mathematical	—	Set Set.instMembership commutatorSet Bracket.bracket commutatorElement	—	—
mem_commutatorSet_of_isConj_sq 📖	mathematical	IsConj DivInvMonoid.toMonoid Group.toDivInvMonoid Monoid.toNatPow	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

---

← Back to Index