map_dvd_map — Mathlib

English

If x Monic, then x.map f divides y.map f iff x divides y, provided f is injective.

Русский

Если x мономический, то x.map f делит y.map f тогда и только тогда, когда x делит y, при условии инъективности f.

LaTeX

$$$$ x \\text{ monic} \\Rightarrow (x.map f \\mid y.map f) \\iff (x \\mid y), $$$$

Lean4

theorem map_dvd_map [Ring S] (f : R →+* S) (hf : Function.Injective f) {x y : R[X]} (hx : x.Monic) :
    x.map f ∣ y.map f ↔ x ∣ y :=
  by
  rw [← modByMonic_eq_zero_iff_dvd hx, ← modByMonic_eq_zero_iff_dvd (hx.map f), ← map_modByMonic f hx]
  exact ⟨fun H => map_injective f hf <| by rw [H, Polynomial.map_zero], fun H => by rw [H, Polynomial.map_zero]⟩

Похожие утверждения