mul_right_inj_of_comparable — Mathlib

English

If left multiplication is strictly mono and b, c are comparable, then a·c = a·b iff c=b.

Русский

Если левая строго монотонна и b, c сравнимы, то a·c = a·b ⇔ c=b.

LaTeX

$$$$ \\forall a,b,c \\in \\alpha,\n [MulLeftStrictMono \\alpha] (b \\le c \\lor c \\le b) \\Rightarrow a \\cdot c = a \\cdot b \\iff c=b $$$$

Lean4

@[to_additive]
theorem mul_right_inj_of_comparable [MulLeftStrictMono α] {a b c : α} (h : b ≤ c ∨ c ≤ b) : a * c = a * b ↔ c = b :=
  by
  refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_left' (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_left' (h.lt_of_ne h') a |>.ne

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