noZeroDivisors_iff_isDomain_or_subsingleton

English

For a ring α, NoZeroDivisors α holds exactly when α is a domain or α is a subsingleton.

Русский

Для кольца α свойство NoZeroDivisors выполняется тогда и только тогда, когда α является доменом или подсинглтон.

LaTeX

$$$$ \\text{NoZeroDivisors}(\\alpha) \\iff \\text{IsDomain}(\\alpha) \\lor \\text{Subsingleton}(\\alpha). $$$$

Lean4

theorem noZeroDivisors_iff_isDomain_or_subsingleton [Ring α] : NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α := by
  rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton]

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