iterateFrobeniusEquiv_add — Mathlib

English

The map for m+n is the transitive composition of the m and n maps: iterateFrobeniusEquiv R p (m+n) = (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m).

Русский

Коэффициентная карта для m+n равна композиции последовательностей: (m+n)-й итеративный Фробениус равен транспозиции n и m.

LaTeX

$$iterateFrobeniusEquiv R p (m+n) = (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m)$$

Lean4

theorem iterateFrobeniusEquiv_add :
    iterateFrobeniusEquiv R p (m + n) = (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m) :=
  RingEquiv.ext (iterateFrobeniusEquiv_add_apply R p m n)

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