charP

Mathlib.Algebra.CharP.Basic

URI: https://scilib.ai/kg/mathlib#Fin.charP

← MathLib Explorer

English

The characteristic of the finite field F_p is p, provided p ≠ 0.

Русский

Характеристика конечного поля F_p равна p, если p ≠ 0.

LaTeX

$$[NeZero p] : CharP (Fin p) p$$

Lean4

/-- The characteristic of `F_p` is `p`. -/
@[stacks 09FS "First part. We don't require `p` to be a prime in mathlib."]
instance charP (n : ℕ) [NeZero n] : CharP (Fin n) n where cast_eq_zero_iff _ := natCast_eq_zero

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

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

Разделы

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

Аффилиация

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