instLeftCancelSemigroup — Mathlib

English

The product of two left-cancel semigroups is left-cancel; i.e., mul_left_cancel holds coordinatewise.

Русский

Произведение двух левосторонне отменяющих полугрупп также левосторонне отменяющее; выполняется свойство mul_left_cancel по компонентам.

LaTeX

$$[LeftCancelSemigroup G] [LeftCancelSemigroup H] ⇒ LeftCancelSemigroup (G × H)$$

Lean4

@[to_additive]
instance [LeftCancelSemigroup G] [LeftCancelSemigroup H] : LeftCancelSemigroup (G × H) :=
  { mul_left_cancel := fun _ _ _ => mul_left_cancel }

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