iterateFrobenius_one

Mathlib.Algebra.CharP.Frobenius

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

English

The one-step iterate equals the Frobenius endomorphism: iterateFrobenius R p 1 = frobenius R p.

Русский

Одношаговая итерация равна Фробениусу: iterateFrobenius R p 1 = frobenius R p.

LaTeX

$$$\\\\iterateFrobenius R p 1 = \\\\ frobenius R p$$$

Lean4

@[simp]
theorem iterateFrobenius_one : iterateFrobenius R p 1 = frobenius R p :=
  RingHom.ext (iterateFrobenius_one_apply R p)

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

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

Разделы

Аффилиация

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