iterateFrobeniusEquiv_symm — Mathlib

English

The inverse of the n-th iterate of Frobenius equals the n-th power of the inverse equivalence: (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n.

Русский

Обратная к n-й итерации Фробениуса равна n-й степени обратной эквивалентности: (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n.

LaTeX

$$$ (iterateFrobeniusEquiv\ R\ p\ n).symm = (frobeniusEquiv\ R\ p).symm ^ n. $$$

Lean4

theorem iterateFrobeniusEquiv_symm : (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n := by
  rw [iterateFrobeniusEquiv_eq_pow]; exact (inv_pow _ _).symm

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