commutatorMap_surjective — Mathlib

English

If φ is fixed-point-free and the group G is finite, then the commutator map g ↦ [g, φ(g)] is surjective onto G.

Русский

Если φ — фикс-фри и группа G конечна, то отображение коммутатора покрывает всю G.

LaTeX

$$$\text{FixedPointFree}(\varphi) \land [\text{Finite } G] \Rightarrow \operatorname{Surjective}(\operatorname{commutatorMap}(\varphi))$$$

Lean4

theorem commutatorMap_surjective (hφ : FixedPointFree φ) : Function.Surjective (commutatorMap φ) :=
  Finite.surjective_of_injective hφ.commutatorMap_injective

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