R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
⊢ degree p < degree q
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
⊢ degree p < degree q
have := EuclideanDomain.div_add_mod p q
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
⊢ degree p < degree q
rwa [h, MulZeroClass.mul_zero, zero_add, mod_eq_self_iff hq0] at this
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
hlt : degree p < degree (q * ↑C (leadingCoeff q)⁻¹)
⊢ p / q = 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
⊢ p / q = 0
have hlt : degree p < degree (q * C (leadingCoeff q)⁻¹) := by
  rwa [degree_mul_leadingCoeff_inv q hq0]
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
hlt : degree p < degree (q * ↑C (leadingCoeff q)⁻¹)
hm : Monic (q * ↑C (leadingCoeff q)⁻¹)
⊢ p / q = 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
hlt : degree p < degree (q * ↑C (leadingCoeff q)⁻¹)
⊢ p / q = 0
have hm : Monic (q * C (leadingCoeff q)⁻¹) := monic_mul_leadingCoeff_inv hq0
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
hlt : degree p < degree (q * ↑C (leadingCoeff q)⁻¹)
hm : Monic (q * ↑C (leadingCoeff q)⁻¹)
⊢ p / q = 0
rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, MulZeroClass.mul_zero]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : degree p < degree q
⊢ degree p < degree (q * ↑C (leadingCoeff q)⁻¹)
rwa [degree_mul_leadingCoeff_inv q hq0]