contentIdeal_le_span_content — Mathlib

English

The content ideal of p is contained in the ideal generated by p.content.

Русский

Контент-идеал p ⊆ порождение множества {p.content}.

LaTeX

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

Lean4

theorem contentIdeal_le_span_content : p.contentIdeal ≤ span { p.content } :=
  by
  rw [contentIdeal_def, span_le]
  intro _ h1
  rw [Finset.mem_coe, mem_coeffs_iff] at h1
  obtain ⟨n, _, h2⟩ := h1
  rw [SetLike.mem_coe, h2, mem_span_singleton]
  exact content_dvd_coeff n

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