coe_sup — Mathlib

English

The top element of HomogeneousIdeal corresponds to the universal set A; its underlying set equals all of A.

Русский

Верхний элемент HomogeneousIdeal соответствует всему кольцу A; его множество равняется A.

LaTeX

$$$\\text{coe\_top}:\\ ((⊤ : HomogeneousIdeal 𝒜) : Set A) = \\mathrm{univ}$$$

Lean4

@[simp]
theorem coe_sup (I J : HomogeneousIdeal 𝒜) : ↑(I ⊔ J) = (I + J : Set A) :=
  Submodule.coe_sup _ _

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