isLeftRegular — Mathlib

English

If a is cancellable on the left, then left multiplication by a is a left-regular operation.

Русский

Если слева отменяемо по отношению к a, тогда умножение слева на a является леворегулярной операцией.

LaTeX

$$$MulLECancellable(a) \Rightarrow IsLeftRegular(a)$$$

Lean4

@[to_additive]
protected theorem isLeftRegular [Mul α] [PartialOrder α] {a : α} (ha : MulLECancellable a) : IsLeftRegular a :=
  ha.Injective

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