Mathlib Map

Theorems · Definition · group theory

commutatorElement

{G : Type u_1} → [Group G] → Bracket G G

The commutator of two elements g₁ and g₂. This is a scoped instance in the commutatorElement namespace to avoid clashing with other brackets.

Defined in
Mathlib.Algebra.Group.Commutator
Cited by
41 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Subgroup.commutator_mem_commutator · cited by 13Subgroup.commutator_mem_c…Subgroup.commutator_le · cited by 10Subgroup.commutator_lecommutatorElement_def · cited by 10commutatorElement_defmap_commutatorElement · cited by 4map_commutatorElementCommute.commutator_eq · cited by 3Commute.commutator_eqSubgroup.focalSubgroup_def · cited by 3Subgroup.focalSubgroup_defcommutatorElement_eq_one_iff_mul_comm · cited by 3commutatorElement_eq_one_…Subgroup.mem_upperCentralSeries_succ_iff · cited by 2Subgroup.mem_upperCentral…commutatorElement_one_left · cited by 1commutatorElement_one_leftcommutatorElement_self · cited by 1commutatorElement_selfSubgroup.mem_upperCentralSeriesStep · cited by 1Subgroup.mem_upperCentral…commutator_mem_commutatorSet · cited by 1commutator_mem_commutator…Matrix.commutator_diag2_transvection · cited by 1Matrix.commutator_diag2_t…Subgroup.mem_lowerCentralSeries_succ_iff · cited by 1Subgroup.mem_lowerCentral…Subgroup.commutator_def · cited by 1Subgroup.commutator_defGroup · cited by 6238GroupBracket · cited by 8BracketcommutatorElementCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Groupstatement and proof · cited by 6,238
  • Bracketstatement · cited by 8

Cited by41

Results whose statement or proof uses this declaration.