xInTermsOfW_vars_subset

Mathlib.RingTheory.WittVector.WittPolynomial

URI: https://scilib.ai/kg/mathlib#xInTermsOfW_vars_subset

English

For prime p, the variables of xInTermsOfW p ℚ n are contained in range(n+1).

Русский

Для простого p переменные xInTermsOfW p ℚ n лежат в диапазоне {0,1,...,n}.

LaTeX

$$$ (xInTermsOfW\ p\ ℚ\ n).vars \subseteq \operatorname{range}(n+1) $$$

Lean4

theorem xInTermsOfW_vars_subset (n : ℕ) : (xInTermsOfW p ℚ n).vars ⊆ range (n + 1) :=
  (xInTermsOfW_vars_aux p n).2

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

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

Разделы

Аффилиация

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