chore(compatibility): compatibility with Lean 3.5.0c (#1007)

leanprover-community · May 11, 2019 · c7d870e · c7d870e
1 parent 60da4f4
commit c7d870e
Show file tree

Hide file tree

Showing 2 changed files with 132 additions and 130 deletions.
diff --git a/src/algebra/ring.lean b/src/algebra/ring.lean
@@ -220,6 +220,8 @@ def nonzero_comm_semiring.of_ne [comm_semiring α] {x y : α} (h : x ≠ y) : no
   zero_ne_one := λ h01, h $ by rw [← one_mul x, ← one_mul y, ← h01, zero_mul, zero_mul],
   ..show comm_semiring α, by apply_instance }
 
+def has_div_of_division_ring [division_ring α] : has_div α := division_ring_has_div
+
 /-- A domain is a ring with no zero divisors, i.e. satisfying
   the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. Alternatively, a domain
   is an integral domain without assuming commutativity of multiplication. -/