instIsSeparatedOfIsAffine

Mathlib.AlgebraicGeometry.Morphisms.Separated

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

English

If X is affine, then X is separated.

Русский

Если X аффина, то X разделима.

LaTeX

$$X.IsSeparated$$

Lean4

instance (priority := 900) {X : Scheme.{u}} [IsAffine X] : X.IsSeparated :=
  ⟨inferInstance⟩

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

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

Разделы

Аффилиация

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