to_isDomain — Mathlib

English

If R is a ring with no zero divisors and nontrivial, then R is a domain.

Русский

Если кольцо не имеет нулевых делителей и не тривиально, то оно является областью целостности.

LaTeX

$$$[\text{Ring } \alpha]\; [\text{Nontrivial } \alpha]\; [\text{NoZeroDivisors } \alpha] \Rightarrow \text{IsDomain } \alpha$$$

Lean4

theorem to_isDomain [Ring α] [h : Nontrivial α] [NoZeroDivisors α] : IsDomain α :=
  { NoZeroDivisors.to_isCancelMulZero α, h with .. }

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