range — Mathlib

English

The range (image) of a monoid homomorphism from a group is a subgroup of the codomain.

Русский

Образ гомоморфизма моноидов от группы является подгруппой кодоцикла.

LaTeX

$$$\operatorname{Im}(f) \le N$ (i.e. the image is a subgroup of the codomain)$$

Lean4

/-- The range of a monoid homomorphism from a group is a subgroup. -/
@[to_additive /-- The range of an `AddMonoidHom` from an `AddGroup` is an `AddSubgroup`. -/
    ]
def range (f : G →* N) : Subgroup N :=
  Subgroup.copy ((⊤ : Subgroup G).map f) (Set.range f) (by simp)

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