instIsCancelMulZeroOfIsCancelAddOfUniqueProds

English

Let R be a semiring and A a monoid with UniqueProds and additive cancellation. Then MonoidAlgebra(R,A) has the cancellation-with-zero property: if f ≠ 0 and f·g = 0, then g = 0.

Русский

Пусть R — полугруппа с нулём, A — моноид с UniqueProds, а также выполняются условия отмены сложения. Тогда MonoidAlgebra(R,A) обладает свойством отмены при умножении на ноль: если f ≠ 0 и f·g = 0, то g = 0.

LaTeX

$$∀ f,g ∈ \\mathrm{MonoidAlgebra}(R,A), f ≠ 0 ∧ (f g = 0) ⇒ g = 0.$$

Lean4

instance [IsCancelAdd R] [IsCancelMulZero R] [Mul A] [UniqueProds A] : IsCancelMulZero (MonoidAlgebra R A) where

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