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✝ : Semiring S
f : R →+* S
hf : Function.Surjective ↑f
p✝ p q : S[X]
hp : ∃ a, map f a = p
hq : ∃ a, map f a = q
p' : R[X]
hp' : map f p' = p
q' : R[X]
hq' : map f q' = q
⊢ map f (p' + q') = p + q
rw [Polynomial.map_add f, hp', hq']
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✝ : Semiring S
f : R →+* S
hf : Function.Surjective ↑f
p : S[X]
n : ℕ
s : S
r : R
hr : ↑f r = s
⊢ map f (↑(monomial n) r) = ↑(monomial n) s
rw [map_monomial f, hr]