iterateFrobenius_comm — Mathlib

English

The iterated Frobenius endomorphism commutes with any ring homomorphism: g ∘ iterateFrobenius R p n = iterateFrobenius S p n ∘ g.

Русский

Итеративный Фробениус-коммутативность: g ∘ iterateFrobenius_{R,p,n} = iterateFrobenius_{S,p,n} ∘ g.

LaTeX

$$$g \circ \operatorname{iterateFrobenius}_{R,p}(n) = \operatorname{iterateFrobenius}_{S,p}(n) \circ g$$$

Lean4

/-- The iterated Frobenius endomorphism commutes with any ring homomorphism. -/
theorem iterateFrobenius_comm (n : ℕ) : g.comp (iterateFrobenius R p n) = (iterateFrobenius S p n).comp g :=
  ext fun x ↦ map_iterateFrobenius g p x n

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