Subset_Product_within_Commutative_Structure_is_Commutative
Provedcommutativityproofwikisubset-products
If the binary operation on a magma is commutative, then the induced operation on the power set is also commutative.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Algebra.Group.Defs
Formal statement
theorem Subset_Product_within_Commutative_Structure_is_Commutative {α : Type _} [Mul α] (hcomm : ∀ a b : α, a * b = b * a) (A B : Set α) : (Set.image2 (· * ·) A B) = (Set.image2 (· * ·) B A) := by sorrySource