isPrimitive_iff_contentIdeal_eq_top

English

In a Bezout ring, a polynomial p is primitive iff its content ideal equals ⊤.

Русский

В Bezout-кольце полином p примитивен тогда и только тогда, когда contentIdeal(p) = ⊤.

LaTeX

$$$p.IsPrimitive \iff p.contentIdeal = \top$$$

Lean4

/-- The polynomial `p` is primitive if and only if the coefficients of `p` generate the whole ring.
-/
theorem isPrimitive_iff_contentIdeal_eq_top : p.IsPrimitive ↔ p.contentIdeal = ⊤ :=
  (IsBezout.isPrincipal_of_FG _ p.contentIdeal_FG).isPrimitive_iff_contentIdeal_eq_top

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