default_asIdeal

Mathlib.AlgebraicGeometry.Scheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.default_asIdeal

English

In Spec of a field K, the default point has the bottom ideal.

Русский

В Spec(.of K) базовая точка имеет минимальный идеал.

LaTeX

$$$ \mathrm{default} : \mathrm{Spec}(.of K).\mathrm{asIdeal} = \mathbf{0}. $$$

Lean4

@[simp]
theorem default_asIdeal {K} [Field K] : (default : Spec (.of K)).asIdeal = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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