mul_right_inj — Mathlib

English

Left-multiplication by a unit is injective on the underlying set: (a·a_unit) = (b·a_unit) implies a = b.

Русский

Левое умножение на единицу инъективно на множествах: a·u = b·u ⇒ a=b.

LaTeX

$$$\forall a,b,c\in \alpha:\; (a\cdot a^{\mathsf{val}} = b\cdot a^{\mathsf{val}}) \iff a=b$$$

Lean4

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

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