mul_left_cancel_iff_of_pos — Mathlib

English

If PosMulReflectLE α and a > 0, then a·b = a·c implies b = c; i.e., left cancellation holds for positive left-multiplication.

Русский

Если PosMulReflectLE α и a > 0, то a·b = a·c ⇒ b = c; то есть слева выполнено отменение для положительного множителя.

LaTeX

$$$a>0 \Rightarrow (a\cdot b = a\cdot c \iff b=c)$ under PosMulReflectLE$$

Lean4

theorem mul_left_cancel_iff_of_pos [PosMulReflectLE α] (a0 : 0 < a) : a * b = a * c ↔ b = c :=
  ⟨fun h => (le_of_mul_le_mul_of_pos_left h.le a0).antisymm <| le_of_mul_le_mul_of_pos_left h.ge a0, congr_arg _⟩

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