instIsLeftCancelMulZeroOfIsCancelAddOfUniqueSums

English

If R is a ring with IsCancelAdd and IsLeftCancelMulZero, and A has unique sums, then AddMonoidAlgebra R A has IsLeftCancelMulZero.

Русский

Если R имеет отменяемость сложения и левую отменяемость по умножению на ноль, и A имеет уникальные суммы, то AddMonoidAlgebra R A обладает IsLeftCancelMulZero.

LaTeX

$$$\text{IsLeftCancelMulZero}(\mathrm{AddMonoidAlgebra}\;R\;A)$$$

Lean4

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

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