R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1237620
B' : Type ?u.1237623
a✝ b : R
n : ℕ
inst✝⁹ : CommSemiring A'
inst✝⁸ : Semiring B'
inst✝⁷ : CommSemiring R
p✝ q✝ : R[X]
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type ?u.1237836
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
x : A
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : eval a (map (algebraMap S T) p) = 0
⊢ eval a (map (algebraMap S T) q) = 0
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1237620
B' : Type ?u.1237623
a✝ b : R
n : ℕ
inst✝⁹ : CommSemiring A'
inst✝⁸ : Semiring B'
inst✝⁷ : CommSemiring R
p✝ q✝ : R[X]
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type ?u.1237836
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
x : A
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : ↑(aeval a) p = 0
⊢ ↑(aeval a) q = 0
rw [aeval_def, ← eval_map] at h₂⊢
no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1237620
B' : Type ?u.1237623
a✝ b : R
n : ℕ
inst✝⁹ : CommSemiring A'
inst✝⁸ : Semiring B'
inst✝⁷ : CommSemiring R
p✝ q✝ : R[X]
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type ?u.1237836
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
x : A
inst✝² : CommSemiring S
inst✝¹ : CommSemiring T
inst✝ : Algebra S T
p q : S[X]
h₁ : p ∣ q
a : T
h₂ : eval a (map (algebraMap S T) p) = 0
⊢ eval a (map (algebraMap S T) q) = 0
exact eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂