div_right_injective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem div_right_injective : Function.Injective fun a ↦ b / a := by
  -- FIXME see above

  simp only [div_eq_mul_inv]
  exact fun a a' h ↦ inv_injective (mul_right_injective b h)

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