no goals
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
simp [eval₂_eq_sum, sum_def]
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
let this : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
no goals
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
simp [this]
no goals
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
simpa using hi'
no goals
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
simp_rw [f.map_mul, f.map_pow, pow_add, mul_pow, mul_assoc]
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
hi : i ∈ support p
⊢ i ≤ natDegree p
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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)
rw [mul_assoc, mul_left_comm, tsub_add_cancel_of_le]
no goals
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : S[X]
f : S →+* R
r : R
s : S
i : ℕ
hi : i ∈ support p
⊢ i ≤ natDegree p
exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)
no goals
A : Type ?u.37521
K : Type ?u.37524
R : Type u_2
S : Type u_1
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
simp [eval₂_eq_sum, sum_def]