toIsRightCancelMul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Not an instance, to avoid loops with `IsRightCancelMul.mulRightStrictMono_of_mulRightMono`. -/
@[to_additive]
theorem toIsRightCancelMul [MulRightStrictMono α] : IsRightCancelMul α where
  mul_right_cancel _ _ _ h := mul_left_strictMono.injective h

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