← Copula mathematical handbook

Finite monoids are Dedekind-finite

instance instIsDedekindFiniteMonoidOfFinite (M : Type u_1) [Monoid M] [Finite M] : IsDedekindFiniteMonoid M