English
Let R be a commutative semiring, p a prime, and m,n nonnegative integers. If R has characteristic p and R is a perfect ring with respect to p, then the inverse of the (m+n)-th iterate of the Frobenius equivalence equals the composition of the inverses of the m-th and n-th iterates in the reverse order; i.e., the (m+n)-th inverse Frobenius equals the n-th inverse Frobenius composed with the m-th inverse Frobenius.
Русский
Пусть R — коммутативное полугруппа-колцо, p — простое число, m, n неотрицательные целые. Если характеристика R равна p и R является совершенным кольцом относительно p, то обратимое отображение, отвечающее за (m+n)-ю итерацию Фробениуса, равно композиции обратимых отображений для n и m в указанном порядке; т.е. (итерационная) обратная Фробениуса для (m+n) равна композиции обратной Фробениуса для n и m.
LaTeX
$$$ (iterateFrobeniusEquiv\ R\ p\ (m+n)).^{-1} = (iterateFrobeniusEquiv\ R\ p\ n)^{-1} \circ (iterateFrobeniusEquiv\ R\ p\ m)^{-1}. $$$
Lean4
theorem iterateFrobeniusEquiv_symm_add :
(iterateFrobeniusEquiv R p (m + n)).symm =
(iterateFrobeniusEquiv R p n).symm.trans (iterateFrobeniusEquiv R p m).symm :=
RingEquiv.ext (iterateFrobeniusEquiv_symm_add_apply R p m n)
