iterateFrobeniusEquiv_one_apply — Mathlib

English

Let x be an element of R. The first iterate of Frobenius equals the p-th power map: iterateFrobeniusEquiv R p 1 x = x^p.

Русский

Пусть x ∈ R. Первая итерация Фробениуса равна отображению возведения в степенную p: iterateFrobeniusEquiv R p 1 x = x^p.

LaTeX

$$$ iterateFrobeniusEquiv\ R\ p\ 1\ x = x^p. $$$

Lean4

theorem iterateFrobeniusEquiv_one_apply (x : R) : iterateFrobeniusEquiv R p 1 x = x ^ p := by
  rw [iterateFrobeniusEquiv_def, pow_one]

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