iterateFrobeniusEquiv_add_apply — Mathlib

English

For m, n, the (m+n)-th iterate evaluated at x equals applying the n-th iterate to the result of applying the m-th iterate to x.

Русский

Для неотрицательных m, n: (m+n)-й итерат Фробениуса к x равен применению n-й итерации к результату применения m-й итерации к x.

LaTeX

$$iterateFrobeniusEquiv R p (m + n) x = iterateFrobeniusEquiv R p n (iterateFrobeniusEquiv R p m x)$$

Lean4

theorem iterateFrobeniusEquiv_add_apply (x : R) :
    iterateFrobeniusEquiv R p (m + n) x = iterateFrobeniusEquiv R p m (iterateFrobeniusEquiv R p n x) :=
  iterateFrobenius_add_apply R p m n x

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