Cuter functions

Changes

1 changed files (+2/-2)

• Set.lean
  • @@ -2,7 +2,7 @@ import Mathlib
    open symmDiff - instance : Add (Set α) := ⟨fun a b ↦ a ∆ b⟩ + instance : Add (Set α) := ⟨(· ∆ ·)⟩ @[simp] lemma add_def {a b : Set α} : a + b = a ∆ b := rfl
  • @@ -17,7 +17,7 @@ instance : Neg (Set α) := ⟨id⟩
    @[simp] lemma neg_def {a : Set α} : -a = a := rfl - instance : Mul (Set α) := ⟨fun a b ↦ a ∩ b⟩ + instance : Mul (Set α) := ⟨(· ∩ ·)⟩ @[simp] lemma mul_def {a b : Set α} : a * b = a ∩ b := rfl