isDomain

Mathlib.Algebra.Ring.Rat

URI: https://scilib.ai/kg/mathlib#Rat.isDomain

English

ℚ is a domain (no zero divisors).

Русский

ℚ — домен: не существует нулевых делителей.

LaTeX

$$$ \\text{IsDomain } \\mathbb{Q}. $$$

Lean4

instance isDomain : IsDomain ℚ :=
  NoZeroDivisors.to_isDomain _

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

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

Разделы

Аффилиация

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