mul_pow_charP_coeff_succ — Mathlib

English

For Witt vectors x and natural m, n, (x · p^n).coeff (m + n) = x.coeff m^{p^n}.

Русский

Для Witt-вектора x и натуральных m, n выполняется (x · p^n).coeff (m + n) = x.coeff m^{p^n}.

LaTeX

$$$ (x \cdot p^n).coeff (m + n) = x.coeff m ^ {p^n} $$$

Lean4

theorem mul_pow_charP_coeff_succ [CharP R p] (x : 𝕎 R) {m n : ℕ} : (x * p ^ n).coeff (m + n) = x.coeff m ^ (p ^ n) := by
  induction n generalizing m with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ← mul_assoc, ← add_assoc, mul_charP_coeff_succ, pow_succ, pow_mul]
    congr
    exact ih

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