isDomain_iff_noZeroDivisors_and_nontrivial

English

For a ring α, IsDomain α is equivalent to NoZeroDivisors α and Nontrivial α.

Русский

Для кольца α равносильно IsDomain α и NoZeroDivisors α вместе с не тривиальностью.

LaTeX

$$$$ \\text{IsDomain}(\\alpha) \\iff \\bigl(\\text{NoZeroDivisors}(\\alpha) \\wedge \\text{Nontrivial}(\\alpha)\\bigr). $$$$

Lean4

theorem isDomain_iff_noZeroDivisors_and_nontrivial [Ring α] : IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α := by
  rw [← isCancelMulZero_iff_noZeroDivisors, isDomain_iff_cancelMulZero_and_nontrivial]

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