iterateFrobeniusEquiv_zero — Mathlib

English

The zero iterate of the Frobenius equivalence is the identity map on the ring R; i.e., iterateFrobeniusEquiv R p 0 = RingEquiv.refl R.

Русский

Нулевая итерация эквивалентности Фробениуса равна тождественному отображению на R: iterateFrobeniusEquiv R p 0 = RingEquiv.refl R.

LaTeX

$$$ iterateFrobeniusEquiv\ R\ p\ 0 = RingEquiv.refl\ R. $$$

Lean4

@[simp]
theorem iterateFrobeniusEquiv_zero : iterateFrobeniusEquiv R p 0 = RingEquiv.refl R :=
  RingEquiv.ext (iterateFrobeniusEquiv_zero_apply R p)

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