mulLECancellable — Mathlib

English

If a is an IsUnit in a monoid with order, then a is MulLECancellable, i.e., left multiplication by a is order-preserving.

Русский

Если a is IsUnit в моноиде с порядком, тогда a имеет свойство MulLECancellable, то есть левое умножение на a сохраняет порядок.

LaTeX

$$IsUnit(a) ⇒ MulLECancellable(a)$$

Lean4

theorem mulLECancellable : MulLECancellable a :=
  ha.unit.mulLECancellable_val

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