commutator_subset_ker — Mathlib

English

For any group homomorphism f: G → A into an abelian group A, the commutator subgroup [G,G] is contained in the kernel of f.

Русский

Для любого гомоморфизма f: G → A в абеллианову группу A, коммутаторная подгруппа [G,G] содержится в ядре f.

LaTeX

$$$$ [G,G] \\leq \\ker f $$ for any MonoidHom f: G →* A with A abelian.$$

Lean4

theorem commutator_subset_ker : commutator G ≤ f.ker :=
  by
  rw [commutator_eq_closure, Subgroup.closure_le]
  rintro x ⟨p, q, rfl⟩
  simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]

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