commGroupOfInjective — Mathlib

English

If G is a group, H is commutative, and f: G →* H is injective, then G is commutative.

Русский

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

LaTeX

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

Lean4

/-- If `H` is commutative and `G →* H` is injective, then `G` is commutative. -/
def commGroupOfInjective [Group G] [CommGroup H] (f : G →* H) (hf : Function.Injective f) : CommGroup G :=
  ⟨by simp_rw [← hf.eq_iff, map_mul, mul_comm, implies_true]⟩

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