monic_map_iff — Mathlib

English

For a polynomial p and injective ring hom f, p.map f is monic if and only if p is monic.

Русский

Для многочлена p и инъективного гомоморфизма f p.map f моничен тогда и только тогда, когда p моничен.

LaTeX

$$$(p.map f).Monic \iff p.Monic$.$$

Lean4

theorem monic_map_iff [Semiring S] [Nontrivial S] {f : R →+* S} {p : R[X]} : (p.map f).Monic ↔ p.Monic := by
  rw [Monic, leadingCoeff_map, ← f.map_one, Function.Injective.eq_iff f.injective, Monic]

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