charP

Mathlib.RingTheory.Perfection

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

English

If p is a prime and p is not a unit in O, then ModP(O,p) has characteristic p.

Русский

Если p — простое и p не является единицей в O, то ModP(O,p) имеет характеристику p.

LaTeX

$$$\operatorname{char}(\mathrm{ModP}(O,p)) = p$$$

Lean4

instance charP [Fact p.Prime] [hvp : Fact (¬IsUnit (p : O))] : CharP (ModP O p) p :=
  CharP.quotient O p <| hvp.1

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

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

Разделы

Аффилиация

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