instRightCancelSemigroup — Mathlib

English

The product of two right-cancel semigroups is right-cancel; i.e., mul_right_cancel holds coordinatewise.

Русский

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

LaTeX

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

Lean4

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

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