of_mul_right — Mathlib

English

If a·b is cancellable, then b is cancellable in a semigroup with left-mono.

Русский

Если a·b — cancellable, то b — cancellable в полугруппе с левым моно.

LaTeX

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

Lean4

@[to_additive]
theorem of_mul_right [Semigroup α] [MulLeftMono α] {a b : α} (h : MulLECancellable (a * b)) : MulLECancellable b :=
  fun c d hcd ↦ h <| by rw [mul_assoc, mul_assoc]; exact mul_le_mul_left' hcd _

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