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
⊢ map f (p / q) = map f p / map f q
if hq0 : q = 0 then simp [hq0]
else
  rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
    Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]
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 [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
  Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]