toIsLeftCancelMul — Mathlib

English

If left multiplication by any element is strictly monotone, then left cancellation holds: a·b1 = a·b2 implies b1 = b2.

Русский

При строго монотонном слева умножении выполняется левое сокращение: если a·b1 = a·b2, то b1 = b2.

LaTeX

$$$\\forall a,b_1,b_2:\; a\cdot b_1 = a\cdot b_2 \Rightarrow b_1 = b_2$$$

Lean4

/-- Not an instance, to avoid loops with `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono`. -/
@[to_additive]
theorem toIsLeftCancelMul [MulLeftStrictMono α] : IsLeftCancelMul α where
  mul_left_cancel _ _ _ h := mul_right_strictMono.injective h

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