contentIdeal_C

Mathlib.RingTheory.Polynomial.ContentIdeal

URI: https://scilib.ai/kg/mathlib#Polynomial.contentIdeal_C

English

The content ideal of a constant polynomial C(r) is the span of r.

Русский

Контент-идеал константы $C(r)$ равен порождению $\{r\}$, то есть $\operatorname{span}\{r\}$.

LaTeX

$$$\operatorname{contentIdeal}(C\;r) = \operatorname{span}\{ r \}$$$

Lean4

@[simp]
theorem contentIdeal_C (r : R) : (C r).contentIdeal = span { r } :=
  by
  rw [← monomial_zero_left]
  exact contentIdeal_monomial 0 r

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru