instIsDomain

Mathlib.Algebra.Field.ZMod

URI: https://scilib.ai/kg/mathlib#ZMod.instIsDomain

English

If p is prime, then ZMod p is an integral domain (and in fact a field).

Русский

Если p простое, то ZMod p — интегральная область (и, фактически, поле).

LaTeX

$$If p is prime, then ZMod p is an integral domain.$$

Lean4

/-- `ZMod p` is an integral domain when `p` is prime. -/
instance : IsDomain (ZMod p) := by constructor

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

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

Разделы

Аффилиация

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