Some facts about finite rings

theorem card_units_lt (M₀ : Type u_1) [MonoidWithZero M₀] [Nontrivial M₀] [Fintype M₀] : Fintype.card M₀ˣ < Fintype.card M₀