Commutative_Semigroup_is_Entropic_Structure

import Mathlib.Algebra.Group.Basic

theorem Commutative_Semigroup_is_Entropic_Structure {S : Type _} [CommSemigroup S] : ∀ a b c d : S, (a * b) * (c * d) = (a * c) * (b * d) := by sorry