iterate_frobenius_coeff — Mathlib

English

Verschiebung and Frobenius are related by Verschiebung(Frobenius x) = x · p; this holds coefficientwise.

Русский

Verschiebung и Frobenius связаны формулой Verschiebung(Frobenius x) = x · p; это выполняется по коэффициентам.

LaTeX

$$$ \mathrm{verschiebung}(\mathrm{frobenius}(x)) = x \cdot p $$$

Lean4

theorem iterate_frobenius_coeff (x : 𝕎 R) (i k : ℕ) : (frobenius^[i] x).coeff k = x.coeff k ^ p ^ i := by
  induction i with
  | zero => simp
  | succ i ih => rw [iterate_succ_apply', coeff_frobenius_charP, ih]; ring_nf

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