Some facts about finite rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
card_units_lt
(M₀ : Type u_1)
[monoid_with_zero M₀]
[nontrivial M₀]
[fintype M₀] :
fintype.card M₀ˣ < fintype.card M₀