eq_top_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 = \top \;\iff\; I.toIdeal = \top $$$

Lean4

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

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