mem_irrelevant_iff — Mathlib

English

An element a lies in the irrelevant ideal if and only if its zero-th homogeneous component vanishes.

Русский

Элемент a принадлежит иррелевантному идеалу тогда и только тогда, когда его нулевая однородная компонента равна нулю.

LaTeX

$$$$ a \in \operatorname{irrelevant}_{\mathcal{A}} \iff (\operatorname{proj}_{0}^{\mathcal{A}} a) = 0. $$$$

Lean4

@[simp]
theorem mem_irrelevant_iff (a : A) : a ∈ HomogeneousIdeal.irrelevant 𝒜 ↔ proj 𝒜 0 a = 0 :=
  Iff.rfl

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