Use instance of HAdd for +

leanprover-community · Sep 18, 2024 · 3d43f4c · 3d43f4c
1 parent 615909b
commit 3d43f4c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -39,8 +39,8 @@ protected def Sum (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α
     | Sum.inl _, Sum.inr _ | Sum.inr _, Sum.inl _ => id
   loopless u := by cases u <;> simp
 
-/-- Disjoint sum of `G` and `H`. -/
-infixl:60 " + " => SimpleGraph.Sum
+@[simps]
+instance : HAdd (SimpleGraph α) (SimpleGraph β) (SimpleGraph (α ⊕ β)) := ⟨SimpleGraph.Sum⟩
 
 variable {G : SimpleGraph α} {H : SimpleGraph β}