English
The range of a finite monoid under a monoid homomorphism is finite.
Русский
Область значения конечного моноида под моноидным гомоморфизмом конечна.
LaTeX
$$$\operatorname{Fintype}(\mathrm{mrange}(f))$$$
Lean4
/-- The range of a finite monoid under a monoid homomorphism is finite.
Note: this instance can form a diamond with `Subtype.fintype` in the
presence of `Fintype N`. -/
@[to_additive /-- The range of a finite additive monoid under an additive monoid homomorphism is
finite.
Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the presence
of `Fintype N`. -/
]
instance fintypeMrange {M N : Type*} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N] (f : M →* N) :
Fintype (mrange f) :=
Set.fintypeRange f
