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)