Theorems · Theorem · group theory
Commute.left_comm
∀ {S : Type u_3} [inst : Semigroup S] {a b : S}, Commute a b → ∀ (c : S), a * (b * c) = b * (a * c)- Defined in
- Mathlib.Algebra.Group.Commute.Defs
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
- Assumes
- Semigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Commutestatement and proof · cited by 639
- Semigroupstatement and proof · cited by 202
- Commute.eqproof · cited by 91
Cited by9
Results whose statement or proof uses this declaration.
- Commute.mul_mul_mul_commproof · cited by 8
- List.prod_insertIdxproof · cited by 2
- Polynomial.scaleRoots_eval₂_mul_of_commuteproof · cited by 2
- List.prod_map_negproof · cited by 2
- HopfAlgebra.antipode_comp_mul_comp_commproof · cited by 1
- Commute.inv_mul_eq_inv_mul_iff_of_isUnitproof · cited by 1
- AddMonoidAlgebra.liftNC_mulproof · cited by 1
- Finset.sum_pow_eq_sum_piAntidiag_of_commuteproof · cited by 1
- MonoidAlgebra.liftNC_mulproof · cited by 0