coe_frobeniusAlgHom

Mathlib.FieldTheory.Finite.Basic

URI: https://scilib.ai/kg/mathlib#FiniteField.coe_frobeniusAlgHom

English

The underlying function of the Frobenius K-algebra equivalence on R is x ↦ x^q.

Русский

Функция-функционал эквивалентности Фробениуса K на R действует как x ↦ x^q.

LaTeX

$$AlgEquiv.funLike.coe (FiniteField.frobeniusAlgEquiv K R) = (λ x, x^q)$$

Lean4

theorem coe_frobeniusAlgHom : ⇑(frobeniusAlgHom K R) = (· ^ q) :=
  rfl

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

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

Разделы

Аффилиация

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