isPrimitive_iff_contentIdeal_eq_top

English

Under the Bezout condition, p is primitive if and only if its content ideal is the top ideal.

Русский

При условии Bezout-фактора, многочлен p примитивен тогда и только тогда, когда его contentIdeal равен ⊤.

LaTeX

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

Lean4

theorem _root_.Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top (h_prin : p.contentIdeal.IsPrincipal) :
    p.IsPrimitive ↔ p.contentIdeal = ⊤ :=
  by
  refine ⟨?_, fun h ↦ isPrimitive_of_contentIdeal_eq_top h⟩
  contrapose!
  simp only [IsPrimitive, not_forall]
  intro _
  use h_prin.generator, h_prin.contentIdeal_generator_dvd
  simp_all [← Ideal.span_singleton_eq_top]

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