A : Type u_1
K : Type u_2
R : Type ?u.42738
S : Type ?u.42741
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
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ eval₂ (algebraMap A K) (↑(algebraMap A K) (num A x)) (scaleRoots p ↑(den A x)) = 0
A : Type u_1
K : Type u_2
R : Type ?u.42738
S : Type ?u.42741
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
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ IsRoot (scaleRoots p ↑(den A x)) (num A x)
apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)
A : Type u_1
K : Type u_2
R : Type ?u.42738
S : Type ?u.42741
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
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval (mk' K (num A x) (den A x))) p = 0
A : Type u_1
K : Type u_2
R : Type ?u.42738
S : Type ?u.42741
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
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ eval₂ (algebraMap A K) (↑(algebraMap A K) (num A x)) (scaleRoots p ↑(den A x)) = 0
refine' scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero _
A : Type u_1
K : Type u_2
R : Type ?u.42738
S : Type ?u.42741
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
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval x) p = 0
A : Type u_1
K : Type u_2
R : Type ?u.42738
S : Type ?u.42741
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
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval (mk' K (num A x) (den A x))) p = 0
rw [mk'_num_den]
no goals
A : Type u_1
K : Type u_2
R : Type ?u.42738
S : Type ?u.42741
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
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : ↑(aeval x) p = 0
⊢ ↑(aeval x) p = 0
exact hr