instIsRightCancelMulZeroOfIsCancelAddOfUniqueSums

English

Let R be a semiring with cancellation on addition and right-cancel multiplication by zero, and let A be an additive monoid with UniqueSums. Then the monoid algebra R[A] inherits the right-cancellation property with respect to multiplication by nonzero elements: if x ≠ 0 and x·y = x·z, then y = z.

Русский

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

LaTeX

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

Lean4

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

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