instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds

English

Under the same hypotheses as above, the monoid algebra MonoidAlgebra(R,A) has the right-cancellation property: if g1 ≠ g2 and g1·f = g2·f for some f ≠ 0, then g1 = g2.

Русский

При тех же предпосылках моноидальная алгебра MonoidAlgebra(R,A) обладает правым свойством отмены: если g1 ≠ g2 и g1·f = g2·f при некотором f ≠ 0, то g1 = g2.

LaTeX

$$$\\forall g_1,g_2,f \\in \\mathrm{MonoidAlgebra}(R,A),\\ f \\neq 0 \\land (g_1 f = g_2 f) \\Rightarrow g_1 = g_2.$$$

Lean4

instance [IsCancelAdd R] [IsRightCancelMulZero R] [Mul A] [UniqueProds A] : IsRightCancelMulZero (MonoidAlgebra R A) :=
  MulOpposite.isLeftCancelMulZero_iff.mp <|
    MonoidAlgebra.opRingEquiv.injective.isLeftCancelMulZero _ (map_zero _) (map_mul _)

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