homogeneousHull_toIdeal_eq_self

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

URI: https://scilib.ai/kg/mathlib#HomogeneousIdeal.homogeneousHull_toIdeal_eq_self

← MathLib Explorer

English

For a homogeneous ideal I, I.toIdeal.homogeneousHull 𝒜 = I.

Русский

Для однородного I верно: I.toIdeal.homogeneousHull 𝒜 = I.

LaTeX

$$$ I.toIdeal.homogeneousHull 𝒜 = I $$$

Lean4

@[simp]
theorem homogeneousHull_toIdeal_eq_self (I : HomogeneousIdeal 𝒜) : I.toIdeal.homogeneousHull 𝒜 = I :=
  HomogeneousIdeal.toIdeal_injective <| I.isHomogeneous.toIdeal_homogeneousHull_eq_self

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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