isPrimitive_iff_content_eq_one — Mathlib

English

For any polynomial p in R[X], p is primitive if and only if its content is equal to 1.

Русский

Для любого многочлена p над кольцом R выполняется: p примитивен тогда и только тогда, когда содержимое p равно 1.

LaTeX

$$$\text{IsPrimitive}(p) \iff p.content = 1$$$

Lean4

theorem isPrimitive_iff_content_eq_one {p : R[X]} : p.IsPrimitive ↔ p.content = 1 :=
  by
  rw [← normalize_content, normalize_eq_one, IsPrimitive]
  simp_rw [← dvd_content_iff_C_dvd]
  exact ⟨fun h => h p.content (dvd_refl p.content), fun h r hdvd => isUnit_of_dvd_unit hdvd h⟩

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