verschiebung_frobenius — Mathlib

English

Verschiebung and Frobenius are related by the identity Verschiebung(Frobenius x) = x · p.

Русский

Verschiebung и Frobenius связаны равенством Verschiebung(Frobenius x) = x · p.

LaTeX

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

Lean4

theorem verschiebung_frobenius [CharP R p] (x : 𝕎 R) : verschiebung (frobenius x) = x * p :=
  by
  ext ⟨i⟩
  · rw [mul_charP_coeff_zero, verschiebung_coeff_zero]
  · rw [mul_charP_coeff_succ, verschiebung_coeff_succ, coeff_frobenius_charP]

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