iterateFrobeniusEquiv_one — Mathlib

English

For natural n, the n-th iterate of Frobenius equals the n-th power of the Frobenius equivalence; i.e., iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n.

Русский

Для натурального n - равна nth итерация Фробениуса степени n равенству: iterateFrobeniusEquiv R p n = frobeniusEquiv R p ^ n.

LaTeX

$$$ iterateFrobeniusEquiv\ R\ p\ n = frobeniusEquiv\ R\ p ^ n. $$$

Lean4

@[simp]
theorem iterateFrobeniusEquiv_one : iterateFrobeniusEquiv R p 1 = frobeniusEquiv R p :=
  RingEquiv.ext (iterateFrobeniusEquiv_one_apply R p)

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