isDomain — Mathlib

English

If A is an integral domain, then its fraction ring K is also an integral domain.

Русский

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

LaTeX

$$IsDomain(K)$$

Lean4

/-- A `CommRing` `K` which is the localization of an integral domain `R` at `R - {0}` is an
integral domain. -/
protected theorem isDomain : IsDomain K :=
  isDomain_of_le_nonZeroDivisors _ (le_refl (nonZeroDivisors A))

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