toIdeal_homogeneousCore_le

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

URI: https://scilib.ai/kg/mathlib#Ideal.toIdeal_homogeneousCore_le

English

If I is homogeneous, then the underlying ideal of its homogeneousCore equals I.

Русский

Если I гомогенен, то подлежащий идеал его homogeneousCore равен I.

LaTeX

$$(I.homogeneousCore 𝒜 I)^{\mathrm{toIdeal}} = I$$

Lean4

theorem toIdeal_homogeneousCore_le : (I.homogeneousCore 𝒜).toIdeal ≤ I :=
  Ideal.homogeneousCore'_le 𝒜 I

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru