Some facts about finite rings

ink

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