feat(algebra/euclidean_domain): div_zero

src/algebra/euclidean_domain.lean

@@ -12,6 +12,7 @@ universe u
 
 class euclidean_domain (α : Type u) extends nonzero_comm_ring α :=
 (quotient : α → α → α)
+(quotient_zero : ∀ a, quotient a 0 = 0)
 (remainder : α → α → α)
  -- This could be changed to the same order as int.mod_add_div.
  -- We normally write qb+r rather than r + qb though.
@@ -98,6 +99,9 @@ mod_eq_zero.2 (dvd_zero _)
 @[simp] lemma zero_div {a : α} (a0 : a ≠ 0) : 0 / a = 0 :=
 by simpa only [zero_mul] using mul_div_cancel 0 a0
 
+@[simp] lemma div_zero (a : α) : a / 0 = 0 :=
+quotient_zero a
+
 @[simp] lemma div_self {a : α} (a0 : a ≠ 0) : a / a = 1 :=
 by simpa only [one_mul] using mul_div_cancel 1 a0
 
@@ -232,6 +236,7 @@ end gcd
 
 instance : euclidean_domain ℤ :=
 { quotient := (/),
+  quotient_zero := int.div_zero,
   remainder := (%),
   quotient_mul_add_remainder_eq := λ a b, by rw add_comm; exact int.mod_add_div _ _,
   r := λ a b, a.nat_abs < b.nat_abs,

src/data/polynomial.lean

@@ -1678,6 +1678,7 @@ div_by_monic_eq_div p (monic_X_sub_C a) ▸ mul_div_by_monic_eq_iff_is_root
 
 instance : euclidean_domain (polynomial α) :=
 { quotient := (/),
+  quotient_zero := by simp [div_def],
   remainder := (%),
   r := _,
   r_well_founded := degree_lt_wf,
@@ -1703,9 +1704,6 @@ lemma div_eq_zero_iff (hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q :=
   have hm : monic (q * C (leading_coeff q)⁻¹) := monic_mul_leading_coeff_inv hq0,
   by rw [div_def, (div_by_monic_eq_zero_iff hm (ne_zero_of_monic hm)).2 hlt, mul_zero]⟩
 
-@[simp] lemma div_zero : p / 0 = 0 :=
-by simp [div_def]
-
 lemma degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) :
   degree q + degree (p / q) = degree p :=
 have degree (p % q) < degree (q * (p / q)) :=