mem_homogeneousCore_of_homogeneous_of_mem

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

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

← MathLib Explorer

English

If x is homogeneous and x ∈ I, then x ∈ homogeneousCore 𝒜 I.

Русский

Если x гомогенный и x ∈ I, тогда x ∈ homogeneousCore 𝒜 I.

LaTeX

$$x ∈ I ∧ IsHomogeneousElem 𝒜 x ⇒ x ∈ I.homogeneousCore 𝒜$$

Lean4

theorem mem_homogeneousCore_of_homogeneous_of_mem {x : A} (h : SetLike.IsHomogeneousElem 𝒜 x) (hmem : x ∈ I) :
    x ∈ I.homogeneousCore 𝒜 :=
  Ideal.subset_span ⟨⟨x, h⟩, hmem, rfl⟩

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

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

Разделы

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

Аффилиация

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