commGroupOfSurjective — Mathlib

English

If G is commutative and f: G →* H is surjective, then H is commutative.

Русский

Если G коммутативна и f: G →* H сюръективен, тогда H коммутативна.

LaTeX

$$$$ \forall a,b \in H,\ ab = ba. $$$$

Lean4

/-- If `G` is commutative and `G →* H` is surjective, then `H` is commutative. -/
def commGroupOfSurjective [CommGroup G] [Group H] (f : G →* H) (hf : Function.Surjective f) : CommGroup H :=
  ⟨by simp_rw [hf.forall₂, ← map_mul, mul_comm, implies_true]⟩

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