bind₁_frobeniusPolyRat_wittPolynomial

English

For all n, applying bind₁ to frobeniusPolyRat with the Witt polynomial yields the Witt polynomial with index n+1 over ℚ.

Русский

Для всех n применение bind₁ к frobeniusPolyRat и Witt-polynomial даёт Witt-polynomial с индексом n+1 над ℚ.

LaTeX

$$$\forall n \in \mathbb{N},\; \text{bind}_1(\operatorname{frobeniusPolyRat}(p))(\mathrm{wittPolynomial}(p,\mathbb{Q},n)) = \mathrm{wittPolynomial}(p,\mathbb{Q},n+1).$$$

Lean4

theorem bind₁_frobeniusPolyRat_wittPolynomial (n : ℕ) :
    bind₁ (frobeniusPolyRat p) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1) :=
  by
  delta frobeniusPolyRat
  rw [← bind₁_bind₁, bind₁_xInTermsOfW_wittPolynomial, bind₁_X_right, Function.comp_apply]

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