instBot

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

URI: https://scilib.ai/kg/mathlib#HomogeneousIdeal.instBot

English

There exists a bottom element in the poset of homogeneous ideals, namely the zero ideal.

Русский

Существует нижний элемент в частично упорядоченном множестве однородных идеалов, равный нулевому идеалу.

LaTeX

$$$\\text{Bot}(\\mathrm{HomogeneousIdeal}) = \\{0\\}$$$

Lean4

instance : Bot (HomogeneousIdeal 𝒜) :=
  ⟨⟨⊥, Ideal.IsHomogeneous.bot 𝒜⟩⟩

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

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

Разделы

Аффилиация

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