mul_right_cancel_iff_of_pos — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_right_cancel_iff_of_pos [MulPosReflectLE α] (b0 : 0 < b) : a * b = c * b ↔ a = c :=
  ⟨fun h => (le_of_mul_le_mul_of_pos_right h.le b0).antisymm <| le_of_mul_le_mul_of_pos_right h.ge b0,
    congr_arg (· * b)⟩

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