instTop — Mathlib

English

There exists a top element in the poset of homogeneous ideals, namely the whole ring A considered as a homogeneous ideal.

Русский

Существет наибольший элемент в частично упорядоченном множестве однородных идеалов, а именно сам весь кольцо A в виде однородного идеала.

LaTeX

$$$\\text{Top}(\\mathrm{HomogeneousIdeal}) = \\text{the whole ring}$$$

Lean4

instance : Top (HomogeneousIdeal 𝒜) :=
  ⟨⟨⊤, Ideal.IsHomogeneous.top 𝒜⟩⟩

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