mul_left_inj — Mathlib

English

Right-multiplication by a unit is injective: b·a = c·a implies b=c for units.

Русский

Правое умножение на единицу инъективно: b·a = c·a ⇒ b=c для единиц.

LaTeX

$$$\forall a\in \alpha^{\times}, \forall b,c\in \alpha:\; b\,a = c\,a \iff b=c$$$

Lean4

@[to_additive (attr := simp)]
theorem mul_left_inj (a : αˣ) {b c : α} : b * a = c * a ↔ b = c :=
  ⟨fun h => by simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h,
    congr_arg (· * a.val)⟩

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