R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x p * eval₂ f x q = 0
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x (p * q) = 0
rw [eval₂_mul f x]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x p * eval₂ f x q = 0
exact mul_eq_zero_of_left hp (q.eval₂ f x)