map_eq_zero — Mathlib

English

For any ring hom f, p.map f = 0 if and only if p = 0, when the target ring is a semiring with nontrivial elements.

Русский

Для любого гомоморфизма кольца f: p.map f = 0 тогда и только тогда, когда p = 0 (при условии, что целевое кольцо не тривиально).

LaTeX

$$$p.map\ f = 0 \iff p = 0.$$$

Lean4

@[simp]
protected theorem map_eq_zero [Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0 :=
  by
  simp only [Polynomial.ext_iff]
  congr!
  simp [map_eq_zero, coeff_map, coeff_zero]

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