wittAdd_vars — Mathlib

English

The variables of the Witt addition polynomial wittAdd p n are contained in the product of the universes for indexing by all positions up to n.

Русский

Переменные многочлена сложения Витта wittAdd p n ограничены произведением универсальных индексов до n.

LaTeX

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

Lean4

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

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