Theorems · Theorem · group theory
Commute.eq
∀ {S : Type u_3} [inst : Mul S] {a b : S}, Commute a b → a * b = b * aEquality behind Commute a b; useful for rewriting.
- Defined in
- Mathlib.Algebra.Group.Commute.Defs
- Cited by
- 91 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 and proof · cited by 639
Cited by91
Results whose statement or proof uses this declaration.
- Polynomial.derivative_mulproof · cited by 35
- Nat.cast_commproof · cited by 16
- Commute.add_powproof · cited by 12
- Module.End.mapsTo_genEigenspace_of_commproof · cited by 10
- Commute.left_commproof · cited by 9
- Commute.isNilpotent_mul_leftproof · cited by 7
- Polynomial.coeff_X_mulproof · cited by 6
- IsSelfAdjoint.commute_iffproof · cited by 5
- Equiv.Perm.nodup_toListproof · cited by 5
- Rat.cast_divInt_of_ne_zeroproof · cited by 5
- Rat.cast_injectiveproof · cited by 5
- Commute.div_add_divproof · cited by 5