iterateFrobenius_add — Mathlib

English

The Frobenius iterates respect addition of the exponent as a composition of maps: iterateFrobenius R p (m+n) = (iterateFrobenius R p m) ∘ (iterateFrobenius R p n).

Русский

Итерация Фробениуса по сумме степеней равна композиции соответствующих итераций: iterateFrobenius R p (m+n) = (iterateFrobenius R p m) ∘ (iterateFrobenius R p n).

LaTeX

$$$\iterateFrobenius R p (m+n) = (\iterateFrobenius R p m) \circ (\iterateFrobenius R p n)$$$

Lean4

theorem iterateFrobenius_add : iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n) :=
  RingHom.ext (iterateFrobenius_add_apply R p m n)

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