wittZSMul_vars — Mathlib

English

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

Русский

Полином ZSMul Витта wittZSMul p m n имеет переменные в Finset.univ ×ˢ Finset.range (n+1).

LaTeX

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

Lean4

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

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