The units of a countable monoid are countable

Mathlib has Finite αˣ for a finite monoid (Mathlib/Algebra/GroupWithZero/Units/Fintype.lean) but no countable analogue, so Countable Mˣ does not resolve even when M is countable. Both follow the same way, from Units.val being injective.

Main results

• Units.instCountable: Mˣ is countable whenever M is.

instance Units.instCountable {M : Type u_1} [Monoid M] [Countable M] : Countable Mˣ

The units of a countable monoid form a countable type, since Units.val is injective.

This is the countable analogue of Mathlib's Finite αˣ, and is proved the same way. Without it Countable Mˣ fails to synthesize, which in turn blocks Countable (GL n R) for a countable ring R — GL n R is by definition (Matrix n n R)ˣ.