wittNSMul_vars — Mathlib

English

The Witt non-scalar multiplication polynomial wittNSMul p m n has its variables contained in Finset.univ ×ˢ Finset.range (n+1).

Русский

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

LaTeX

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

Lean4

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

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