instNoZeroDivisors

Mathlib.Algebra.GroupWithZero.WithZero

URI: https://scilib.ai/kg/mathlib#WithZero.instNoZeroDivisors

English

The type WithZero α has no zero divisors; i.e., x*y = 0 implies x = 0 or y = 0.

Русский

Тип WithZero α не имеет нулевых делителей: x*y = 0 влечёт x = 0 или y = 0.

LaTeX

$$$\\text{NoZeroDivisors}(\\text{WithZero } \\alpha)$$$

Lean4

instance instNoZeroDivisors : NoZeroDivisors (WithZero α) :=
  ⟨Option.map₂_eq_none_iff.1⟩

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

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

Разделы

Аффилиация

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