commutatorMap_injective — Mathlib

English

Let φ be a fixed-point-free endomorphism of a group G. Then the commutator map g ↦ [g, φ(g)] is injective.

Русский

Пусть φ — собственная точечно-фиксированная эндоморфизм группы G. Тогда отображение g ↦ [g, φ(g)] инъективно.

LaTeX

$$$\text{FixedPointFree}(\varphi) \Rightarrow \operatorname{Injective}(\operatorname{commutatorMap}(\varphi))$$$

Lean4

theorem commutatorMap_injective (hφ : FixedPointFree φ) : Function.Injective (commutatorMap φ) :=
  by
  refine fun x y h ↦ inv_mul_eq_one.mp <| hφ _ ?_
  rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]

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