contentIdeal_mul_le_mul_contentIdeal

English

The content ideal of a product is contained in the product of content ideals: contentIdeal(p q) ≤ contentIdeal(p) contentIdeal(q).

Русский

Контент-идеал произведения не превосходит произведение контент-идеалов: contentIdeal(p q) ≤ contentIdeal(p) contentIdeal(q).

LaTeX

$$$(p \cdot q).contentIdeal \le p.contentIdeal \cdot q.contentIdeal$$$

Lean4

theorem contentIdeal_mul_le_mul_contentIdeal (q : R[X]) : (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal :=
  by
  rw [contentIdeal_def, span_le]
  simp only [Set.subset_def, Finset.mem_coe, mem_coeffs_iff]
  rintro r ⟨n, _, rfl⟩
  simp [coeff_mul, _root_.sum_mem, Submodule.mul_mem_mul, coeff_mem_contentIdeal]

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