of_mul_left — Mathlib

English

If a·b is cancellable, then a is cancellable (in a commutative semigroup with left-monotone).

Русский

Если a·b — cancellable, то a — cancellable (в коммутативной полугруппе с левой монотонностью).

LaTeX

$$MulLECancellable (a · b) → MulLECancellable a$$

Lean4

@[to_additive]
theorem of_mul_left [CommSemigroup α] [MulLeftMono α] {a b : α} (h : MulLECancellable (a * b)) : MulLECancellable a :=
  (mul_comm a b ▸ h).of_mul_right

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