iterate_verschiebung_coeff_eq_zero

English

Iterating Verschiebung distributes over multiplication for Witt vectors: Verschiebung^i x · Verschiebung^j y = Verschiebung^(i+j) ( Frobenius^j x · Frobenius^i y ).

Русский

Пусть i и j — неотрицательные целые; тогда Verschiebung^i x · Verschiebung^j y = Verschiebung^(i+j) (Frobenius^j x · Frobenius^i y).

LaTeX

$$$ \text{verschiebung}^{i} x \cdot \text{verschiebung}^{j} y = \text{verschiebung}^{i+j} (\text{frobenius}^{j} x \cdot \text{frobenius}^{i} y) $$$

Lean4

theorem iterate_verschiebung_coeff_eq_zero (x : 𝕎 R) {n : ℕ} {m : ℕ} (h : m < n) : (verschiebung^[n] x).coeff m = 0 :=
  by
  induction n generalizing m with
  | zero => contradiction
  | succ n ih =>
    rw [iterate_succ_apply']
    cases m with
    | zero => exact verschiebung_coeff_zero _
    | succ m' =>
      rw [verschiebung_coeff_succ, ih]
      simpa using h

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