iterateFrobenius_zero

Mathlib.Algebra.CharP.Frobenius

URI: https://scilib.ai/kg/mathlib#iterateFrobenius_zero

English

The zero-th iterate of Frobenius is the identity endomorphism on R: iterateFrobenius R p 0 = id_R.

Русский

Нулевой итератор Фробениуса является тождественным эндоморфизмом на R: iterateFrobenius R p 0 = id_R.

LaTeX

$$$\iterateFrobenius R p 0 = \mathrm{id}_R$$$

Lean4

@[simp]
theorem iterateFrobenius_zero : iterateFrobenius R p 0 = RingHom.id R :=
  RingHom.ext (iterateFrobenius_zero_apply R p)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru