contentIdeal_le_span_iff_dvd — Mathlib

English

For a principal content ideal h_prin, p.contentIdeal ≤ span{ r } iff C r divides p.

Русский

Для порожденного contentIdeal: contentIdeal(p) ≤ span{ r } тогда и только тогда C(r) делит p.

LaTeX

$$p.contentIdeal ≤ span\{ r \} \iff C r \mid p$$

Lean4

theorem _root_.Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd (h_prin : p.contentIdeal.IsPrincipal) (r : R) :
    p.contentIdeal ≤ span { r } ↔ C r ∣ p := by
  constructor
  · rw [← p.contentIdeal.span_singleton_generator]
    intro _
    calc
      C r ∣ C h_prin.generator := by
        apply _root_.map_dvd C
        rwa [← span_singleton_le_span_singleton]
      _ ∣ p := h_prin.contentIdeal_generator_dvd
  · rw [← contentIdeal_C r]
    exact fun h ↦ contentIdeal_le_contentIdeal_of_dvd h

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