Documentation

Mathlib.RingTheory.Fintype

Some facts about finite rings #

theorem card_units_lt (M₀ : Type u_1) [inst : MonoidWithZero M₀] [inst : Nontrivial M₀] [inst : Fintype M₀] :