instIsLeftCancelMul — Mathlib

English

If G and H are left-cancellative semigroups, then G × H is left-cancellative; i.e., if (a,b)·(x,y)=(a,b)·(x',y'), then (x,y)=(x',y').

Русский

Если G и H — левосокращающие полугруппы, то их произведение левосторонне сокращает; то есть если (a,b)(x,y)=(a,b)(x',y'), то (x,y)=(x',y').

LaTeX

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

Lean4

@[to_additive]
instance [Mul G] [Mul H] [IsLeftCancelMul G] [IsLeftCancelMul H] : IsLeftCancelMul (G × H) where
  mul_left_cancel _ _ _ h := Prod.ext (mul_left_cancel (Prod.ext_iff.1 h).1) (mul_left_cancel (Prod.ext_iff.1 h).2)

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