iterateFrobenius_eq_pow — Mathlib

English

The iterate Frobenius map equals the nth power of the Frobenius endomorphism: iterateFrobenius R p n = frobenius R p ^ n.

Русский

Преемник Фробениуса равен n-й степени Фробениуса: iterateFrobenius R p n = frobenius R p ^ n.

LaTeX

$$$\\\\iterateFrobenius R p n = (\\\\frobenius R p)^n$$$

Lean4

theorem iterateFrobenius_eq_pow : iterateFrobenius R p n = frobenius R p ^ n := by ext;
  simp [iterateFrobenius_def, iterate_frobenius]

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