Element_Commutes_with_Product_of_Commuting_Elements
Provedassociativitycommutativityproofwiki
In a semigroup (S, ∘), if x commutes with both y and z, then x commutes with y ∘ z.
Preamble
import Mathlib.Algebra.Group.Basic
Formal statement
theorem Element_Commutes_with_Product_of_Commuting_Elements {S : Type _} [Semigroup S] {x y z : S} (hxy : x * y = y * x) (hxz : x * z = z * x) : x * (y * z) = (y * z) * x := by sorrySource