affineBasisCover_obj

Mathlib.AlgebraicGeometry.Cover.Open

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

Lean4

theorem affineBasisCover_obj (X : Scheme.{u}) (i : X.affineBasisCover.I₀) :
    X.affineBasisCover.X i = Spec (X.affineBasisCoverRing i) :=
  rfl

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

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

Разделы

Аффилиация

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