Cardinality of localizations of commutative monoids

This file contains some results on cardinality of localizations.

theorem Localization.cardinalMk_le {M : Type u} [CommMonoid M] (S : Submonoid M) : Cardinal.mk (Localization S) ≤ Cardinal.mk M

theorem AddLocalization.cardinalMk_le {M : Type u} [AddCommMonoid M] (S : AddSubmonoid M) : Cardinal.mk (AddLocalization S) ≤ Cardinal.mk M