Restriction_of_Commutative_Operation_is_Commutative
Provedcommutativityproofwiki
Let (S, ∘) be an algebraic structure with commutative ∘, and T ⊆ S. Then the restriction of ∘ to T is also commutative.
Preamble
import Mathlib.Algebra.Group.Basic import Mathlib.Data.Set.Basic
Formal statement
theorem Restriction_of_Commutative_Operation_is_Commutative {S : Type _} [CommSemigroup S] (T : Set S) : ∀ a b : T, (a : S) * (b : S) = (b : S) * (a : S) := by sorrySource