instIsDomainOfIsCancelAddOfUniqueProds

English

If R is a domain and A is a monoid with UniqueProds, then the monoid algebra MonoidAlgebra(R,A) is a domain (i.e., has no zero divisors).

Русский

Если R — область без нулевых делителей, а A — моноид с UniqueProds, то MonoidAlgebra(R,A) также является областью (без нулевых делителей).

LaTeX

$$IsDomain(\\mathrm{MonoidAlgebra}(R,A)).$$

Lean4

instance [IsCancelAdd R] [IsDomain R] [Monoid A] [UniqueProds A] : IsDomain (MonoidAlgebra R A) where

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