frobeniusEquiv_symm_pow_p — Mathlib

English

For any x ∈ R, the p-th power of the inverse Frobenius image of x equals x; i.e., ((frobeniusEquiv R p).symm x)^p = x.

Русский

Для любого x ∈ R, p-я степень образа обратного Фробениуса равна x: ((frobeniusEquiv R p).symm x)^p = x.

LaTeX

$$$ ((frobeniusEquiv R p).symm x)^p = x. $$$

Lean4

@[simp]
theorem frobeniusEquiv_symm_pow_p (x : R) : ((frobeniusEquiv R p).symm x) ^ p = x :=
  frobenius_apply_frobeniusEquiv_symm R p x

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