iff_eq — Mathlib

English

An ideal is homogeneous iff it can be generated by a set of homogeneous elements.

Русский

Идеал гомогенен тогда и только тогда, когда он порожден множеством однородных элементов.

LaTeX

$$I.IsHomogeneous 𝒜 I ⇔ ∃ S, I = Ideal.span (Set.image Subtype.val S)$$

Lean4

theorem iff_eq : I.IsHomogeneous 𝒜 ↔ (I.homogeneousCore 𝒜).toIdeal = I :=
  ⟨fun hI => hI.toIdeal_homogeneousCore_eq_self, fun hI => hI ▸ (Ideal.homogeneousCore 𝒜 I).2⟩

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