mathlib documentation

ring_theory.fintype

Some facts about finite rings #

theorem card_units_lt (M₀ : Type u_1) [monoid_with_zero M₀] [nontrivial M₀] [fintype M₀] :