A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ leadingCoeff p
suffices (den A r : A) ∣ p.leadingCoeff * num A r ^ p.natDegree by
  refine'
    dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) _
      this
  intro q dvd_den dvd_num_pow hq
  apply hq.not_unit
  exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ coeff (scaleRoots p ?s) (natDegree p) * num A r ^ natDegree p

case s
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ A
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
rw [← coeff_scaleRoots_natDegree]
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ natDegree p → ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ↑(den A r) ∣ coeff (scaleRoots p ?s) (natDegree p) * num A r ^ natDegree p

case s
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ A
apply dvd_term_of_isRoot_of_dvd_terms _ (num_isRoot_scaleRoots_of_aeval_eq_zero hr)
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ natDegree p → ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
intro j hj
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j

case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : ¬j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
by_cases h : j < p.natDegree
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : ¬j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
rw [← natDegree_scaleRoots p (den A r)] at *
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ 0
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne (le_of_not_gt h) hj.symm),
  MulZeroClass.zero_mul]
no goals
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree (scaleRoots p ↑(den A r))
h : ¬j < natDegree (scaleRoots p ↑(den A r))
⊢ ↑(den A r) ∣ 0
exact dvd_zero _
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
⊢ ∀ {d : A}, d ∣ ↑(den A r) → d ∣ num A r ^ natDegree p → ¬Prime d
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
⊢ ↑(den A r) ∣ leadingCoeff p
refine'
  dvd_of_dvd_mul_left_of_no_prime_factors (mem_nonZeroDivisors_iff_ne_zero.mp (den A r).2) _
    this
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ False
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
⊢ ∀ {d : A}, d ∣ ↑(den A r) → d ∣ num A r ^ natDegree p → ¬Prime d
intro q dvd_den dvd_num_pow hq
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ IsUnit q
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ False
apply hq.not_unit
no goals
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
this : ↑(den A r) ∣ leadingCoeff p * num A r ^ natDegree p
q : A
dvd_den : q ∣ ↑(den A r)
dvd_num_pow : q ∣ num A r ^ natDegree p
hq : Prime q
⊢ IsUnit q
exact num_den_reduced A r (hq.dvd_of_dvd_pow dvd_num_pow) dvd_den
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff p j * ↑(den A r) ^ (natDegree p - j) * num A r ^ j
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff (scaleRoots p ↑(den A r)) j * num A r ^ j
rw [coeff_scaleRoots]
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ ↑(den A r) ^ (natDegree p - j)
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ coeff p j * ↑(den A r) ^ (natDegree p - j) * num A r ^ j
refine' (dvd_mul_of_dvd_right _ _).mul_right _
case h.e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) = ↑(den A r) ^ Nat.succ ?pos.convert_1✝

case pos.convert_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ℕ

case pos.convert_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ j + ?pos.convert_1✝ < natDegree p
case pos
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) ∣ ↑(den A r) ^ (natDegree p - j)
convert pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))
no goals
case pos.convert_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ j + 0 < natDegree p
simpa using h
no goals
case h.e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : ↑(aeval r) p = 0
j : ℕ
hj : j ≠ natDegree p
h : j < natDegree p
⊢ ↑(den A r) = ↑(den A r) ^ Nat.succ ?pos.convert_1✝
exact (pow_one _).symm