bind₁_frobeniusPoly_wittPolynomial

English

The map bind₁ of frobeniusPoly with a Witt polynomial over ℤ gives the Witt polynomial one index higher: bind₁ (frobeniusPoly p) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n+1).

Русский

Осуществление bind₁ от frobeniusPoly p с Witt-полином p ℤ даёт Witt-полином с индексом n+1.

LaTeX

$$$\forall n,\; \text{bind}_1 (\operatorname{frobeniusPoly}(p)) (\mathrm{wittPolynomial}(p,\mathbb{Z},n)) = \mathrm{wittPolynomial}(p,\mathbb{Z},n+1).$$$

Lean4

@[simp]
theorem bind₁_frobeniusPoly_wittPolynomial (n : ℕ) :
    bind₁ (frobeniusPoly p) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1) :=
  by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [map_bind₁, map_frobeniusPoly, bind₁_frobeniusPolyRat_wittPolynomial, map_wittPolynomial]

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