frobenius_one

Mathlib.Algebra.CharP.Frobenius

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

English

Frobenius maps the unit to the unit: frobenius R p 1 = 1.

Русский

Фробениус отображает единицу в единицу: frobenius R p 1 = 1.

LaTeX

$$$frobenius R p 1 = 1$$$

Lean4

theorem frobenius_one : frobenius R p 1 = 1 :=
  one_pow _

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

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

Разделы

Аффилиация

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