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_1) [MonoidWithZero M₀] [Nontrivial M₀] [Fintype M₀] : Fintype.card M₀ˣ < Fintype.card M₀

theorem natCard_units_lt (M₀ : Type u_1) [MonoidWithZero M₀] [Nontrivial M₀] [Finite M₀] : Nat.card M₀ˣ < Nat.card M₀

theorem orderOf_lt_card {M₀ : Type u_1} [MonoidWithZero M₀] [Nontrivial M₀] [Finite M₀] (a : M₀) : orderOf a < Nat.card M₀

theorem ZMod.orderOf_lt {n : ℕ} (hn : 1 < n) (a : ZMod n) : orderOf a < n