toIdeal — Mathlib

English

Let 𝒜 be a graded ring and I a homogeneous ideal of 𝒜. Then, when viewed as an ideal of the base ring A (forgetting the grading), I becomes an ordinary ideal of A.

Русский

Пусть 𝒜 — градуированное кольцо, а I — однородный идеал 𝒜. Рассматривая его как идеал над базовым кольцом A (без учёта градации), I образует обычный идеал A.

LaTeX

$$$\text{toIdeal}(I) \text{ is an ideal of } A$$$

Lean4

/-- Converting a homogeneous ideal to an ideal. -/
abbrev toIdeal (I : HomogeneousIdeal 𝒜) : Ideal A :=
  I.toSubmodule

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