wittSub_vars — Mathlib

English

The Witt subtraction polynomial wittSub p n has its variables contained in Finset.univ ×ˢ Finset.range (n+1).

Русский

Полином вычитания Витта wittSub p n имеет переменные, ограниченные Finset.univ ×ˢ Finset.range (n+1).

LaTeX

$$$(wittSub\ p\ n).vars \subseteq \mathrm{Finset.univ} \times^{\!} \mathrm{Finset.range}(n+1)$$$

Lean4

theorem wittSub_vars (n : ℕ) : (wittSub p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1) :=
  wittStructureInt_vars _ _ _

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