range_isMulCommutative — Mathlib

English

If G is a commutative group, then the range of any homomorphism f: G →* N is a commutative submonoid (i.e. its multiplication is commutative).

Русский

Если G коммутативна, образ фоморфизма f: G →* N является коммутативной подмоноидой.

LaTeX

$$IsMulCommutative(f.range)$$

Lean4

@[to_additive]
instance range_isMulCommutative {G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) :
    IsMulCommutative f.range :=
  range_eq_map f ▸ Subgroup.map_isMulCommutative ⊤ f

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