instIsDomainOfIsCancelAddOfUniqueSums

English

If R is a domain and IsCancelAdd R holds, and A is an additive monoid with UniqueSums, then the monoid algebra R[A] is an integral domain.

Русский

Если R является доменом, выполняются условия IsCancelAdd R и A — аддитивный моноид с UniqueSums, то монойдная алгебра R[A] является целостным доменом.

LaTeX

$$$\text{IsDomain} (R[A]).$$$

Lean4

instance [IsCancelAdd R] [IsDomain R] [AddMonoid A] [UniqueSums A] : IsDomain R[A] where

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