map_ne_zero_iff — Mathlib

English

If f is injective, then for any p ∈ R[X], p.map f ≠ 0 if and only if p ≠ 0.

Русский

Если f инъективно, то для любого p ∈ R[X], p.map f ≠ 0 тогда и только тогда, когда p ≠ 0.

LaTeX

$$$\\mathrm{Injective}(f) \\Rightarrow \\forall p \\in R[X],\\ p.map f \\neq 0 \\iff p \\neq 0$$$

Lean4

protected theorem map_ne_zero_iff (hf : Function.Injective f) : p.map f ≠ 0 ↔ p ≠ 0 :=
  (Polynomial.map_eq_zero_iff hf).not

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