R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : DivisionRing R
p q : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
⊢ (∀ (n : ℕ), coeff (map f p) n = coeff 0 n) ↔ ∀ (n : ℕ), coeff p n = coeff 0 n
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : DivisionRing R
p q : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
⊢ map f p = 0 ↔ p = 0
simp only [Polynomial.ext_iff]
case a.h.a
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : DivisionRing R
p q : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
a✝ : ℕ
⊢ coeff (map f p) a✝ = coeff 0 a✝ ↔ coeff p a✝ = coeff 0 a✝
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : DivisionRing R
p q : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
⊢ (∀ (n : ℕ), coeff (map f p) n = coeff 0 n) ↔ ∀ (n : ℕ), coeff p n = coeff 0 n
congr!
no goals
case a.h.a
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : DivisionRing R
p q : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
a✝ : ℕ
⊢ coeff (map f p) a✝ = coeff 0 a✝ ↔ coeff p a✝ = coeff 0 a✝
simp [map_eq_zero, coeff_map, coeff_zero]