Commutator

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

Statistics

Metric	Count
Definitions commutatorElement	1
Theorems commutatorElement_def	1
Total	2

(root)

Definitions

Name	Category	Theorems
commutatorElement 📖	CompOp	19 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, commutatorSet_def, map_commutatorElement, conjugate_commutatorElement, Commute.commutator_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutatorElement_def 📖	mathematical	—	Bracket.bracket commutatorElement MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toInv	—	—

---

← Back to Index