Documentation

Mathlib.GroupTheory.DedekindFinite

Finite monoids are Dedekind-finite #

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