R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
⊢ map f x ∣ map f y ↔ x ∣ y
rw [← dvd_iff_modByMonic_eq_zero hx, ← dvd_iff_modByMonic_eq_zero (hx.map f), ←
  map_modByMonic f hx]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
exact
  ⟨fun H => map_injective f hf <| by rw [H, Polynomial.map_zero], fun H => by
    rw [H, Polynomial.map_zero]⟩
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
H : map f (y %ₘ x) = 0
⊢ map f (y %ₘ x) = map f 0
rw [H, Polynomial.map_zero]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ↑f
x y : R[X]
hx : Monic x
H : y %ₘ x = 0
⊢ map f (y %ₘ x) = 0
rw [H, Polynomial.map_zero]