instIsDomain — Mathlib

English

If R is a domain and M is free, then SymmetricAlgebra R M is a domain.

Русский

Если R — домен и M свободен, то SymmetricAlgebra R M также домен.

LaTeX

$$$[\text{IsDomain } R] \Rightarrow [\text{IsDomain } (\operatorname{Sym}_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 (SymmetricAlgebra R M) :=
  NoZeroDivisors.to_isDomain _

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