[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
i : ℕ
⊢ coeff (scaleRoots p s) i = coeff p i * s ^ (natDegree p - i)
[PROOFSTEP]
simp (config := { contextual := true }) [scaleRoots, coeff_monomial]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ coeff (scaleRoots p s) (natDegree p) = leadingCoeff p
[PROOFSTEP]
rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
s : R
⊢ scaleRoots 0 s = 0
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
s : R
n✝ : ℕ
⊢ coeff (scaleRoots 0 s) n✝ = coeff 0 n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
⊢ scaleRoots p s ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
⊢ False
[PROOFSTEP]
have : p.coeff p.natDegree ≠ 0 := mt leadingCoeff_eq_zero.mp hp
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
this : coeff p (natDegree p) ≠ 0
⊢ False
[PROOFSTEP]
have : (scaleRoots p s).coeff p.natDegree = 0 := congr_fun (congr_arg (coeff : R[X] → ℕ → R) h) p.natDegree
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
this✝ : coeff p (natDegree p) ≠ 0
this : coeff (scaleRoots p s) (natDegree p) = 0
⊢ False
[PROOFSTEP]
rw [coeff_scaleRoots_natDegree] at this 
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
s : R
h : scaleRoots p s = 0
this✝ : coeff p (natDegree p) ≠ 0
this : leadingCoeff p = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ support (scaleRoots p s) ≤ support p
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
a✝ : ℕ
⊢ a✝ ∈ support (scaleRoots p s) → a✝ ∈ support p
[PROOFSTEP]
simpa using left_ne_zero_of_mul
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
⊢ support p ≤ support (scaleRoots p s)
[PROOFSTEP]
intro i
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ support p → i ∈ support (scaleRoots p s)
[PROOFSTEP]
simp only [coeff_scaleRoots, Polynomial.mem_support_iff]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ coeff p i ≠ 0 → coeff p i * s ^ (natDegree p - i) ≠ 0
[PROOFSTEP]
intro p_ne_zero ps_zero
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : coeff p i ≠ 0
ps_zero : coeff p i * s ^ (natDegree p - i) = 0
⊢ False
[PROOFSTEP]
have := pow_mem hs (p.natDegree - i) _ ps_zero
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : coeff p i ≠ 0
ps_zero : coeff p i * s ^ (natDegree p - i) = 0
this : coeff p i = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
rw [hp, zero_scaleRoots]
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ degree (scaleRoots p s) = degree p
[PROOFSTEP]
refine' le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree _)
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ coeff (scaleRoots p s) (natDegree p) ≠ 0
[PROOFSTEP]
rw [coeff_scaleRoots_natDegree]
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ leadingCoeff p ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
⊢ False
[PROOFSTEP]
have := leadingCoeff_eq_zero.mp h
[GOAL]
case neg
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
this✝ : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
this : p = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ natDegree (scaleRoots p s) = natDegree p
[PROOFSTEP]
simp only [natDegree, degree_scaleRoots]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
s : R
⊢ Monic (scaleRoots p s) ↔ Monic p
[PROOFSTEP]
simp only [Monic, leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : ↑f (leadingCoeff p) ≠ 0
⊢ map f (scaleRoots p x) = scaleRoots (map f p) (↑f x)
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : ↑f (leadingCoeff p) ≠ 0
n✝ : ℕ
⊢ coeff (map f (scaleRoots p x)) n✝ = coeff (scaleRoots (map f p) (↑f x)) n✝
[PROOFSTEP]
simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
⊢ eval₂ f (↑f s * r) (scaleRoots p s) =
    ∑ i in support (scaleRoots p s), ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i
[PROOFSTEP]
simp [eval₂_eq_sum, sum_def]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
hi' : ¬i ∈ support (scaleRoots p s)
⊢ ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i = 0
[PROOFSTEP]
let this : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
hi' : ¬i ∈ support (scaleRoots p s)
⊢ coeff p i * s ^ (natDegree p - i) = 0
[PROOFSTEP]
simpa using hi'
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
hi' : ¬i ∈ support (scaleRoots p s)
this : coeff p i * s ^ (natDegree p - i) = 0 :=
  Eq.mp
    (Eq.trans
      (congrArg Not
        (Eq.trans Mathlib.Data.Polynomial.Basic._auxLemma.17 (congrFun (congrArg Ne (coeff_scaleRoots p s i)) 0)))
      Mathlib.Logic.Basic._auxLemma.9)
    hi'
⊢ ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i = 0
[PROOFSTEP]
simp [this]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
_hi : i ∈ support p
⊢ ↑f (coeff p i * s ^ (natDegree p - i)) * (↑f s * r) ^ i = ↑f (coeff p i) * ↑f s ^ (natDegree p - i + i) * r ^ i
[PROOFSTEP]
simp_rw [f.map_mul, f.map_pow, pow_add, mul_pow, mul_assoc]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
hi : i ∈ support p
⊢ ↑f (coeff p i) * ↑f s ^ (natDegree p - i + i) * r ^ i = ↑f s ^ natDegree p * (↑f (coeff p i) * r ^ i)
[PROOFSTEP]
rw [mul_assoc, mul_left_comm, tsub_add_cancel_of_le]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
hi : i ∈ support p
⊢ i ≤ natDegree p
[PROOFSTEP]
exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
⊢ ↑f s ^ natDegree p * ∑ i in support p, ↑f (coeff p i) * r ^ i = ↑f s ^ natDegree p * eval₂ f r p
[PROOFSTEP]
simp [eval₂_eq_sum, sum_def]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* R
r : R
s : S
hr : eval₂ f r p = 0
⊢ eval₂ f (↑f s * r) (scaleRoots p s) = 0
[PROOFSTEP]
rw [scaleRoots_eval₂_mul, hr, mul_zero]
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
⊢ eval₂ f (↑f r) (scaleRoots p s) = 0
[PROOFSTEP]
nontriviality S using Subsingleton.eq_zero
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
✝ : Nontrivial S
⊢ eval₂ f (↑f r) (scaleRoots p s) = 0
[PROOFSTEP]
convert @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr
[GOAL]
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
✝ : Nontrivial S
⊢ ↑f r = ↑f s * (↑f r / ↑f s)
[PROOFSTEP]
rw [← mul_div_assoc, mul_comm, mul_div_cancel]
[GOAL]
case h.e'_2.h.e'_6.h
R : Type u_1
S : Type u_2
A : Type u_3
K : Type u_4
inst✝³ : Semiring S
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ↑f
r s : S
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors S
✝ : Nontrivial S
⊢ ↑f s ≠ 0
[PROOFSTEP]
exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs
