relevant

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant

← MathLib Explorer

English

The ideal I = carrier.asIdeal f_deg hm q is not the whole ring, i.e., I ≠ ⊤.

Русский

Идеал I ≠ ⊤; он не порождает весь кольцо.

LaTeX

$$$carrier.asIdeal f_{deg} hm q \neq \top$$$

Lean4

theorem relevant : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ carrier.asHomogeneousIdeal f_deg hm q := fun rid =>
  carrier.denom_notMem f_deg hm q <| rid <| DirectSum.decompose_of_mem_ne 𝒜 f_deg hm.ne'

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

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

Разделы

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

Аффилиация

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