instIsCancelMulColex — Mathlib

English

Cancellation properties are inherited by Colex: if α has the cancellation property, then Colex α does as well.

Русский

Свойства отмены наследуются Colex: если у α есть свойство отмены, то и Colex α имеет его.

LaTeX

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

Lean4

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

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