contentIdeal_zero — Mathlib

English

Let R be a semiring and p a polynomial in R[X]. The content ideal of the zero polynomial is the bottom submodule: contentIdeal(0) = ⊥.

Русский

Пусть R — полукольцо, p — многочлен из R[X]. Контент-идеал нулевого многочлена равен нижней подмодуль: contentIdeal(0) = ⊥.

LaTeX

$$$\operatorname{contentIdeal}(0) = \bot$$$

Lean4

@[simp]
theorem contentIdeal_zero : (0 : R[X]).contentIdeal = ⊥ := by simp [contentIdeal_def]

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