ne_top

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

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

English

The carrier yields a homogeneous subobject with respect to 𝒜.

Русский

carrier образует однородный подпредмет относительно 𝒜.

LaTeX

$$$(carrier f_{deg} hm q).IsHomogeneous 𝒜$$$

Lean4

theorem ne_top : carrier.asIdeal f_deg hm q ≠ ⊤ := fun rid =>
  carrier.denom_notMem f_deg hm q (rid.symm ▸ Submodule.mem_top)

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

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

Разделы

Аффилиация

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