instIsRightCancelMulOrderDual — Mathlib

English

If α has a right-cancel law, then its order dual αᵒᵈ also satisfies right-cancel: IsRightCancelMul αᵒᵈ.

Русский

Если у α есть правое отменяющее свойство, то его двойственность по порядку αᵒᵈ также имеет правое отменяющее свойство.

LaTeX

$$IsRightCancelMul(α^{\mathrm{op}})$$

Lean4

@[to_additive]
instance [Mul α] [h : IsRightCancelMul α] : IsRightCancelMul αᵒᵈ :=
  h

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