case h.e'_2.h.e
A : Type u_1
K : Type ?u.888
R : Type ?u.891
S : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
⊢ ↑(aeval (↑(algebraMap A S) r)) = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s)
A : Type u_1
K : Type ?u.888
R : Type ?u.891
S : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
⊢ ↑(aeval (↑(algebraMap A S) r)) (scaleRoots p ↑s) = 0
convert scaleRoots_eval₂_eq_zero (algebraMap A S) hr
case h.e'_2.h.e.h
A : Type u_1
K : Type ?u.888
R : Type ?u.891
S : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ ↑(aeval (↑(algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s) x✝
case h.e'_2.h.e
A : Type u_1
K : Type ?u.888
R : Type ?u.891
S : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
⊢ ↑(aeval (↑(algebraMap A S) r)) = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s)
funext
no goals
case h.e'_2.h.e.h
A : Type u_1
K : Type ?u.888
R : Type ?u.891
S : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Field K
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Submonoid A
inst✝³ : Algebra A S
inst✝² : IsLocalization M S
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : A
s : { x // x ∈ M }
hr : ↑(aeval (mk' S r s)) p = 0
x✝ : A[X]
⊢ ↑(aeval (↑(algebraMap A S) r)) x✝ = eval₂ (algebraMap A S) (↑(algebraMap A S) ↑s * mk' S r s) x✝
rw [aeval_def, mk'_spec' _ r s]