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)
:
Finset.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)
:
Finset.univ = {0, 1, -1}
theorem
card_units_lt
(M₀ : Type u_2)
[MonoidWithZero M₀]
[Nontrivial M₀]
[Fintype M₀]
:
Fintype.card M₀ˣ < Fintype.card M₀