Commutator

📁 Source: Mathlib/Algebra/Group/Commutator.lean

Statistics

Metric	Count
Definitions addCommutatorElement, commutatorElement	2
Theorems addCommutatorElement_def, commutatorElement_def	2
Total	4

(root)

Definitions

Name	Category	Theorems
addCommutatorElement 📖	CompOp	19 math math: addCommutatorSet_def, addCommutatorElement_neg, AddSubgroup.addCommutator_mem_addCommutator, AddSubgroup.addCommutator_def, addCommutatorElement_zero_left, AddSubgroup.addCommutator_le, addCommutatorElement_self, AddCommute.addCommutator_eq, addCommutatorElement_def, AddSubgroup.focalAddSubgroupOf_eq_closure, addCommutatorElement_zero_right, map_addCommutatorElement, addCommutator_mem_addCommutatorSet, mem_addCommutatorSet_iff, addCommutatorElement_eq_zero_iff_add_comm, addCommutatorElement_eq_zero_iff_addCommute, AddSubgroup.addCommutator_def', AddSubgroup.focalAddSubgroup_def, conjugate_addCommutatorElement
commutatorElement 📖	CompOp	21 math math: commutatorElement_def, Subgroup.commutator_def', commutatorElement_one_left, commutator_mem_commutatorSet, Subgroup.quotientCentralizerEmbedding_apply, commutatorElement_one_right, Subgroup.commutator_le, mem_commutatorSet_iff, commutatorElement_inv, Subgroup.commutator_mem_commutator, Subgroup.commutator_def, commutatorElement_self, commutatorElement_eq_one_iff_commute, Subgroup.quotientCenterEmbedding_apply, commutatorElement_eq_one_iff_mul_comm, Subgroup.focalSubgroupOf_eq_closure, Subgroup.focalSubgroup_def, commutatorSet_def, map_commutatorElement, conjugate_commutatorElement, Commute.commutator_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addCommutatorElement_def 📖	mathematical	—	Bracket.bracket addCommutatorElement AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toNeg	—	—
commutatorElement_def 📖	mathematical	—	Bracket.bracket commutatorElement MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toInv	—	—

---

← Back to Index