Theorems · Theorem · group theory
commute_iff_eq
∀ {S : Type u_3} [inst : Mul S] (a b : S), Commute a b ↔ a * b = b * aTwo elements a and b commute if a * b = b * a.
- Defined in
- Mathlib.Algebra.Group.Commute.Defs
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Commutestatement · cited by 639
Cited by20
Results whose statement or proof uses this declaration.
- Set.natCast_mem_centerproof · cited by 2
- Commute.cfcHomproof · cited by 2
- Commute.cfcₙHomproof · cited by 2
- Polynomial.smeval_commuteproof · cited by 1
- MvPowerSeries.commute_monomialproof · cited by 1
- Ring.descPochhammer_smeval_addproof · cited by 1
- Commute.of_orderOf_dvd_twoproof · cited by 1
- isStarNormal_iff_commute_realPart_imaginaryPartproof · cited by 1
- Set.intCast_mem_centerproof · cited by 0
- Set.one_mem_centerproof · cited by 0
- RootPairing.isOrthogonal_commproof · cited by 0