contentIdeal_monomial — Mathlib

English

The content ideal of a monomial (monomial n r) is the span of r.

Русский

Контент-идеал монома $(n, r)$ равен порожденному множества $\{r\}$.

LaTeX

$$$\operatorname{contentIdeal}(\text{monomial}(n, r)) = \operatorname{span}\{ r \}$$$

Lean4

@[simp]
theorem contentIdeal_monomial (n : ℕ) (r : R) : (monomial n r).contentIdeal = span { r } := by
  by_cases h : r = 0 <;> simp [h, Set.singleton_zero, contentIdeal_def, coeffs_monomial]

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