Changes
1 changed files (+78/-0)
-
Set.lean (new)
-
@@ -0,0 +1,78 @@import Mathlib open symmDiff -- open Set -- #eval {1, 2, 3} ∆ {3, 6} example [Monoid M] (N : Submonoid M) : Monoid N where mul := fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x*y, N.mul_mem hx hy⟩ mul_assoc := by grind one := ⟨1, N.one_mem⟩ one_mul := fun ⟨x, _⟩ ↦ SetCoe.ext (one_mul x) mul_one := fun ⟨x, _⟩ ↦ SetCoe.ext (mul_one x) #check Set.symmDiff_def #synth Add ℕ -- #synth symmDiff (Set ℕ) (Set ℕ) instance : Add (Set α) := ⟨fun a b ↦ a ∆ b⟩ @[simp] lemma add_def {a b : Set α} : a + b = a ∆ b := rfl instance : Zero (Set α) := ⟨{}⟩ @[simp] lemma zero_def : (0 : Set α) = {} := rfl instance : Neg (Set α) := ⟨id⟩ @[simp] lemma neg_def {a : Set α} : -a = a := rfl instance : Mul (Set α) := ⟨fun a b ↦ a ∩ b⟩ @[simp] lemma mul_def {a b : Set α} : a * b = a ∩ b := rfl instance : One (Set α) := ⟨.univ⟩ @[simp] lemma one_def : (1 : Set α) = .univ := rfl example : CommRing (Set α) where add_assoc := by simp only [add_def] grind zero_add := by simp add_zero := by simp nsmul := nsmulRec zsmul := zsmulRec neg_add_cancel := by simp add_comm := by simp only [add_def] grind left_distrib := by intro a b c ext x simp [symmDiff_def] grind right_distrib := by intro a b c ext x simp [symmDiff_def] grind zero_mul := by simp mul_zero := by simp mul_assoc := by simp only [mul_def] grind one_mul := by simp mul_one := by simp mul_comm := by simp only [mul_def] grind
-