no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : q = 0
⊢ map f (p % q) = map f p % map f q
simp [hq0]
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p % q) = map f p % map f q
rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
  map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]