frobenius

Mathlib.Algebra.CharP.Lemmas

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

← MathLib Explorer

English

For a finite ring R with no zero divisors, the characteristic ringChar(R) is a prime number.

Русский

Для конечного кольца R без нулевых делителей характеристика ringChar(R) простая.

LaTeX

$$Nat.Prime(ringChar(R))$$

Lean4

/-- The Frobenius map `x ↦ x ^ p`. -/
def frobenius : R →+* R where
  __ := powMonoidHom p
  map_zero' := zero_pow (expChar_pos R p).ne'
  map_add' _ _ := add_pow_expChar ..

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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