contentIdeal_eq_span_content_of_isPrincipal

English

If p.contentIdeal is principal, then p.contentIdeal equals span{ p.content }.

Русский

Если contentIdeal(p) порождено, то contentIdeal(p) = span{ p.content }.

LaTeX

$$p.contentIdeal = span\{ p.content \}$$

Lean4

theorem _root_.Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal (h_prin : p.contentIdeal.IsPrincipal) :
    p.contentIdeal = span { p.content } :=
  by
  apply le_antisymm contentIdeal_le_span_content
  rw [← p.contentIdeal.span_singleton_generator, span_singleton_le_span_singleton, content, Finset.dvd_gcd_iff]
  exact fun n _ ↦ h_prin.contentIdeal_generator_dvd_coeff n

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