A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ support p → i ∈ support (scaleRoots p s)
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
⊢ support p ≤ support (scaleRoots p s)
intro i
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ coeff p i ≠ 0 → coeff p i * s ^ (natDegree p - i) ≠ 0
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ support p → i ∈ support (scaleRoots p s)
simp only [coeff_scaleRoots, Polynomial.mem_support_iff]
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ coeff p i ≠ 0 → coeff p i * s ^ (natDegree p - i) ≠ 0
intro p_ne_zero ps_zero
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
have := pow_mem hs (p.natDegree - i) _ ps_zero
no goals
A : Type ?u.32461
K : Type ?u.32464
R : Type u_1
S : Type ?u.32470
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
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
contradiction