Some facts about finite rings

theorem Finset.univ_of_card_le_two {R : Type u_1} [Ring R] [Fintype R] [DecidableEq R] (h : Fintype.card R ≤ 2) : univ = {0, 1}

theorem Finset.univ_of_card_le_three {R : Type u_1} [Ring R] [Fintype R] [DecidableEq R] (h : Fintype.card R ≤ 3) : univ = {0, 1, -1}

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