division_ring_has_div' without double instance

leanprover-community · Mar 26, 2019 · d0e4221 · d0e4221
1 parent a016652
commit d0e4221
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/algebra/field.lean b/src/algebra/field.lean
@@ -9,6 +9,9 @@ open set
 universe u
 variables {α : Type u}
 
+@[priority 101]
+instance division_ring_has_div' [division_ring α] : has_div α := ⟨algebra.div⟩
+
 instance division_ring.to_domain [s : division_ring α] : domain α :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ a b h,
     classical.by_contradiction $ λ hn,