instIsRightCancelMulColex — Mathlib

English

Right-cancellation is preserved by the Colex construction: if α has right-cancellation, then Colex α does as well.

Русский

Правая отмена сохраняется при Colex: если у α есть правая отмена, то и у Colex α она есть.

LaTeX

$$$IsRightCancelMul(\alpha) \Rightarrow IsRightCancelMul(\mathrm{Colex} \alpha)$$$

Lean4

@[to_additive]
instance [Mul α] [IsRightCancelMul α] : IsRightCancelMul (Colex α) :=
  inferInstanceAs <| IsRightCancelMul α

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