instNoZeroDivisorsOfUniqueSums — Mathlib

English

If R has no zero divisors and A has unique sums, then AddMonoidAlgebra R A has no zero divisors.

Русский

Если R не имеет нулевых делителей и A обладает уникальными суммами, то AddMonoidAlgebra R A также не имеет нулевых делителей.

LaTeX

$$$\operatorname{NoZeroDivisors}(\mathrm{AddMonoidAlgebra}\;R\;A)$$$

Lean4

instance [NoZeroDivisors R] [Add A] [UniqueSums A] : NoZeroDivisors R[A] :=
  inferInstanceAs (NoZeroDivisors (MonoidAlgebra R (Multiplicative A)))

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