le_toIdeal_homogeneousHull — Mathlib

English

I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal; the hull is the smallest homogeneous ideal containing I.

Русский

I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal; оболочка — это наименьший однородный идеал, содержащий I.

LaTeX

$$$ I \le (Ideal.homogeneousHull 𝒜 I).toIdeal $$$

Lean4

theorem le_toIdeal_homogeneousHull : I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal :=
  by
  intro r hr
  classical
  rw [← DirectSum.sum_support_decompose 𝒜 r]
  refine Ideal.sum_mem _ ?_
  intro j _
  apply Ideal.subset_span
  use j
  use ⟨r, hr⟩

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