instIsDomain — Mathlib

English

If R is an integral domain, then FreeAlgebra R X is an integral domain.

Русский

Если R — интегральный домен, то FreeAlgebra R X также интегральный домен.

LaTeX

$$$\text{IsDomain } R \Rightarrow \text{IsDomain } \mathrm{FreeAlgebra}(R,X)$$$

Lean4

/-- `FreeAlgebra R X` is a domain when `R` is an integral domain. -/
instance instIsDomain {R X} [CommRing R] [IsDomain R] : IsDomain (FreeAlgebra R X) :=
  NoZeroDivisors.to_isDomain _

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