coe_iterateFrobeniusEquiv

Mathlib.FieldTheory.Perfect

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

English

The underlying function of iterateFrobeniusEquiv R p n is exactly iterateFrobenius R p n.

Русский

Функциональная часть iterateFrobeniusEquiv R p n совпадает с iterateFrobenius R p n.

LaTeX

$$coe_iterateFrobeniusEquiv (R) (p) (n) : equality of functions$$

Lean4

@[simp]
theorem coe_iterateFrobeniusEquiv : ⇑(iterateFrobeniusEquiv R p n) = iterateFrobenius R p n :=
  rfl

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

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

Разделы

Аффилиация

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