instLeftCancelMonoid — Mathlib

English

The product of two left-cancel monoids is left-cancel; in particular, mul_one and one_mul hold, and mul_left_cancel holds for all elements.

Русский

Произведение двух левосторонне отменяющих моноидов — левосторонне отменяющее; в частности выполняются свойства mul_one, one_mul и mul_left_cancel.

LaTeX

$$[LeftCancelMonoid M] [LeftCancelMonoid N] ⇒ LeftCancelMonoid (M × N)$$

Lean4

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

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