contentIdeal_one

Mathlib.RingTheory.Polynomial.ContentIdeal

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

English

The content ideal of the constant polynomial 1 is the top submodule, i.e., contentIdeal(1) = ⊤.

Русский

Контент-идеал константы 1 равен верхней подмодуле: contentIdeal(1) = ⊤.

LaTeX

$$$\operatorname{contentIdeal}(1) = \top$$$

Lean4

@[simp]
theorem contentIdeal_one : (1 : R[X]).contentIdeal = ⊤ := by rw [← span_singleton_one, ← contentIdeal_C 1, C_1]

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

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

Разделы

Аффилиация

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