basicOpen_pow

Mathlib.AlgebraicGeometry.Scheme

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

English

For a positive exponent n, the basic open of f^n equals the basic open of f.

Русский

Для положительного показателя n базовое открытое f^n равно базовому открытому f.

LaTeX

$$$X.basicOpen (f^n) = X.basicOpen f \\quad (n > 0)$$$

Lean4

theorem basicOpen_pow {n : ℕ} (h : 0 < n) : X.basicOpen (f ^ n) = X.basicOpen f :=
  RingedSpace.basicOpen_pow _ _ _ h

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

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

Разделы

Аффилиация

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