instIsCancelMulZeroOfIsCancelAddOfUniqueSums

English

Assume IsCancelAdd R, IsCancelMulZero R, an additive monoid A, and UniqueSums A. Then the monoid algebra R[A] has the cancellation property for multiplication by nonzero elements on the right: if y ≠ 0 and x·y = z·y, then x = z.

Русский

Пусть R удовлетворяет отменяемости по сложению и отменяемости умножения на ноль, A — аддитивный моноид, и A имеет уникальные суммы. Тогда монойдальная алгебра R[A] обладает свойством отмены умножения на ненулевой множитель справа: если y ≠ 0 и x·y = z·y, то x = z.

LaTeX

$$$\forall x,y,z \in R[A],\ y \ne 0 \land x y = z y \Rightarrow x = z.$$$

Lean4

instance [IsCancelAdd R] [IsCancelMulZero R] [Add A] [UniqueSums A] : IsCancelMulZero R[A] where

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