isPrimitive_iff_isUnit_of_C_dvd — Mathlib

English

For a commutative ring R and a polynomial p ∈ R[X], p is primitive iff for every r ∈ R, if C r divides p then r is a unit.

Русский

Для коммутативного кольца R и полинома p ∈ R[X] полином p примитивен тогда и только тогда, когда для каждого r ∈ R, если C r делит p, то r является еденицей (обратимым элементом).

LaTeX

$$$$ p \\text{ is primitive } \\iff \\forall r \\in R,\; C r \\mid p \\rightarrow IsUnit(r) $$$$

Lean4

theorem isPrimitive_iff_isUnit_of_C_dvd {p : R[X]} : p.IsPrimitive ↔ ∀ r : R, C r ∣ p → IsUnit r :=
  Iff.rfl

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