wittPolynomial_vars_subset — Mathlib

English

The set of variables of wittPolynomial p R n is contained in the range {0,...,n}.

Русский

Множество переменных полинома Witt p R n содержится в диапазоне {0,...,n}.

LaTeX

$$(wittPolynomial p R n).vars ⊆ range (n + 1)$$

Lean4

theorem wittPolynomial_vars_subset (n : ℕ) : (wittPolynomial p R n).vars ⊆ range (n + 1) :=
  by
  rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]
  apply vars_map

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