iterate_verschiebung_coeff — Mathlib

English

A specialized form of the projection formula: (verschiebung^i x · verschiebung^j y).coeff (i+j) = p-powers times coefficients of x and y at zero index.

Русский

Узкую форму проективной формулы: (verschiebung^i x · verschiebung^j y).coeff(i+j) = x.coeff 0^{p^j} · y.coeff 0^{p^i}.

LaTeX

$$$ (verschiebung^{i} x \cdot verschiebung^{j} y).coeff (i + j) = x.coeff 0^{p^{j}} \cdot y.coeff 0^{p^{i}} $$$

Lean4

theorem iterate_verschiebung_coeff (x : 𝕎 R) (n k : ℕ) : (verschiebung^[n] x).coeff (k + n) = x.coeff k := by
  induction n with
  | zero => simp
  | succ k ih => rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]; exact ih

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