iterateFrobeniusEquiv_symm_add_apply

English

Applying the inverse of the (m+n)-th iterate to x equals applying the inverses of m and n in reverse order to x.

Русский

Применение обратного (m+n)-й итерации к x эквивалентно применению обратных итераций m и n в обратном порядке к x.

LaTeX

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

Lean4

theorem iterateFrobeniusEquiv_symm_add_apply (x : R) :
    (iterateFrobeniusEquiv R p (m + n)).symm x =
      (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x) :=
  (iterateFrobeniusEquiv R p (m + n)).injective <| by
    rw [RingEquiv.apply_symm_apply, add_comm, iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply,
      RingEquiv.apply_symm_apply]

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