instNoZeroDivisorsCastInt

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.instNoZeroDivisorsCastInt

English

The ring ℤ√d has no zero divisors; i.e., ab = 0 implies a = 0 or b = 0.

Русский

У кольца ℤ√d нет нулевых делителей; то есть ab = 0 тогда либо a = 0, либо b = 0.

LaTeX

$$$$\forall a,b \in \mathbb{Z}\sqrt{d},\; a b = 0 \Rightarrow a = 0 \lor b = 0.$$$$

Lean4

instance : NoZeroDivisors (ℤ√d) where eq_zero_or_eq_zero_of_mul_eq_zero := Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero

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

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

Разделы

Аффилиация

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