monic_map_iff — Mathlib

English

For an injective f, p is monic if and only if p.map f is monic.

Русский

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

LaTeX

$$$\forall {R} {S} [\text{Semiring } R] [\text{Semiring } S] {f : R \rightarrow+* S} (hf : Injective f) {p : R[X]}, p.Monic \leftrightarrow (p.map f).Monic$$$

Lean4

theorem _root_.Function.Injective.monic_map_iff (hf : Injective f) {p : R[X]} : p.Monic ↔ (p.map f).Monic :=
  ⟨Monic.map _, Polynomial.monic_of_injective hf⟩

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