instIsRightCancelMul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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