coe_inf — Mathlib

English

The toIdeal map preserves the top element; the top homogeneous ideal maps to the top ideal of A.

Русский

Отображение toIdeal сохраняет верхний элемент: топовый однородный идеал соответствует топовому идеалу A.

LaTeX

$$$\\text{toIdeal\_top}: (\\top : HomogeneousIdeal 𝒜)\\toIdeal = (\\top : Ideal A)$$$

Lean4

@[simp]
theorem coe_inf (I J : HomogeneousIdeal 𝒜) : (↑(I ⊓ J) : Set A) = ↑I ∩ ↑J :=
  rfl

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