verschiebung_frobenius_comm — Mathlib

English

Verschiebung and Frobenius commute: Verschiebung ∘ Frobenius = Frobenius ∘ Verschiebung.

Русский

Фробениус и Verschiebung коммутируют: Verschiebung ∘ Frobenius = Frobenius ∘ Verschiebung.

LaTeX

$$$ \text{verschiebung} \circ \text{frobenius} = \text{frobenius} \circ \text{verschiebung} $$$

Lean4

theorem verschiebung_frobenius_comm [CharP R p] : Function.Commute (verschiebung : 𝕎 R → 𝕎 R) frobenius := fun x => by
  rw [verschiebung_frobenius, frobenius_verschiebung]

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