isHomogeneous — Mathlib

English

If I is a homogeneous ideal of 𝒜, then its image as an ordinary ideal I.toIdeal is homogeneous with respect to the same grading 𝒜.

Русский

Если I — однородный идеал 𝒜, то соответствующий обычный идеал I.toIdeal остаётся однородным по той же градации 𝒜.

LaTeX

$$$I \text{ is homogeneous } 𝒜 \Rightarrow I^{\mathrm{toIdeal}} \text{ is homogeneous } 𝒜$$$

Lean4

theorem isHomogeneous (I : HomogeneousIdeal 𝒜) : I.toIdeal.IsHomogeneous 𝒜 :=
  I.is_homogeneous'

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