case h.e'_2.h.e'_6
A : Type u_1
K : Type u_2
R : Type ?u.324057
S : Type ?u.324060
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : A[X]
f : A →+* K
hf : Function.Injective ↑f
r s : A
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors A
⊢ ↑f r = ↑f s * (↑f r / ↑f s)
A : Type u_1
K : Type u_2
R : Type ?u.324057
S : Type ?u.324060
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : A[X]
f : A →+* K
hf : Function.Injective ↑f
r s : A
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors A
⊢ eval₂ f (↑f r) (scaleRoots p s) = 0
convert @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr
case h.e'_2.h.e'_6.h
A : Type u_1
K : Type u_2
R : Type ?u.324057
S : Type ?u.324060
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : A[X]
f : A →+* K
hf : Function.Injective ↑f
r s : A
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors A
⊢ ↑f s ≠ 0
case h.e'_2.h.e'_6
A : Type u_1
K : Type u_2
R : Type ?u.324057
S : Type ?u.324060
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : A[X]
f : A →+* K
hf : Function.Injective ↑f
r s : A
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors A
⊢ ↑f r = ↑f s * (↑f r / ↑f s)
rw [← mul_div_assoc, mul_comm, mul_div_cancel]
no goals
case h.e'_2.h.e'_6.h
A : Type u_1
K : Type u_2
R : Type ?u.324057
S : Type ?u.324060
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : A[X]
f : A →+* K
hf : Function.Injective ↑f
r s : A
hr : eval₂ f (↑f r / ↑f s) p = 0
hs : s ∈ nonZeroDivisors A
⊢ ↑f s ≠ 0
exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs