instIsDomain — Mathlib

English

If R is an integral domain and M is a free R-module, then TensorAlgebra R M is an integral domain.

Русский

Если R — целостный домен и M — свободный модуль над R, то TensorAlgebra R M является доменом.

LaTeX

$$$ IsDomain (TensorAlgebra R M) $$$

Lean4

/-- The `TensorAlgebra` of a free module over an integral domain is a domain. -/
instance instIsDomain [IsDomain R] [Module.Free R M] : IsDomain (TensorAlgebra R M) :=
  NoZeroDivisors.to_isDomain _

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