Symmetric_Difference_on_Power_Set_forms_Abelian_Group_v2
Provedabelian-groupspower-setproofwikisymmetric-difference
Let S be a set. The symmetric difference operation on the power set of S forms an abelian group.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Order.SymmDiff
Formal statement
theorem Symmetric_Difference_on_Power_Set_forms_Abelian_Group_v2 {S : Type _} : ∀ A B : Set S, symmDiff A B = symmDiff B A := by sorrySource