English
Let G be a finite group and f: G → N be a group homomorphism. Then the image of G under f, i.e. f(G), is finite.
Русский
Пусть G — конечная группа и f: G → N — гомоморфизм групп. Тогда образ f(G) конечен.
LaTeX
$$$|G| < \infty \Rightarrow |f(G)| < \infty$$$
Lean4
/-- The range of a finite group under a group homomorphism is finite.
Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the
presence of `Fintype N`. -/
@[to_additive /-- The range of a finite additive group under an additive group homomorphism is finite.
Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the
presence of `Fintype N`. -/
]
instance fintypeRange [Fintype G] [DecidableEq N] (f : G →* N) : Fintype (range f) :=
Set.fintypeRange f
