coeff_p_pow — Mathlib

English

In a Witt vector over R with a prime p, the i-th coefficient of (p)^i is 1.

Русский

В витер-векторе над R и простым p, i-й коэффициент (p)^i равен 1.

LaTeX

$$[CharP R p] (coeff of (p : 𝕎 R)^i at i) = 1$$

Lean4

theorem coeff_p_pow [CharP R p] (i : ℕ) : ((p : 𝕎 R) ^ i).coeff i = 1 := by
  induction i with
  | zero => simp only [one_coeff_zero, pow_zero]
  | succ i h => rw [pow_succ, ← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ, h, one_pow]

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