mathlib documentation

ring_theory.fintype

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₀] :