toIdeal_injective — Mathlib

English

The map from homogeneous ideals to ordinary ideals given by toIdeal is injective.

Русский

Отображение однородных идеалов в обычные идеалы через toIdeal инъективно.

LaTeX

$$∀ I J, I^{\mathrm{toIdeal}} = J^{\mathrm{toIdeal}} ⇒ I = J$$

Lean4

theorem toIdeal_injective : Function.Injective (HomogeneousIdeal.toIdeal : HomogeneousIdeal 𝒜 → Ideal A) :=
  HomogeneousSubmodule.toSubmodule_injective 𝒜 𝒜

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