div_left_injective — Mathlib

English

Let G be a group and b ∈ G. The map a ↦ a / b is injective.

Русский

Пусть G — группа и фиксировано b ∈ G. Отображение a ↦ a / b инъективно.

LaTeX

$$$\forall a \in G\, \forall a' \in G\, \forall b \in G,\ a/b = a'/b \Rightarrow a = a'.$$

Lean4

@[to_additive]
theorem div_left_injective : Function.Injective fun a ↦ a / b := by
  -- FIXME this could be by `simpa`, but it fails. This is probably a bug in `simpa`.

  simp only [div_eq_mul_inv]
  exact fun a a' h ↦ mul_left_injective b⁻¹ h

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