instRightCancelMonoid — Mathlib

English

Let M and N be right-cancellative monoids. Then the direct product M × N, with coordinatewise multiplication, is a right-cancellative monoid.

Русский

Пусть M и N — моноиды с правой отменой. Тогда прямое произведение M × N с покомпонентным умножением является моноидом с правой отменой.

LaTeX

$$$(\mathrm{RightCancelMonoid}(M) \wedge \mathrm{RightCancelMonoid}(N)) \implies \mathrm{RightCancelMonoid}(M \times N)$$$

Lean4

@[to_additive]
instance [RightCancelMonoid M] [RightCancelMonoid N] : RightCancelMonoid (M × N) :=
  { mul_one := by simp, one_mul := by simp
    mul_right_cancel _ _ := by simp }

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