eq_bot_iff — Mathlib

English

For any homogeneous ideal I in 𝒜, I = ⊥ if and only if its associated ideal equals ⊥: I = ⊥ ⇔ I.toIdeal = ⊥.

Русский

Для любого однородного идеала I в 𝒜 верно: I = ⊥ тогда и только тогда, когда связанный с ним идеал равен ⊥: I = ⊥ ⇔ I.toIdeal = ⊥.

LaTeX

$$$ I = \bot \;\iff\; I.toIdeal = \bot $$$

Lean4

@[simp]
theorem eq_bot_iff (I : HomogeneousIdeal 𝒜) : I = ⊥ ↔ I.toIdeal = ⊥ :=
  toIdeal_injective.eq_iff.symm

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