English
If |R| ≤ 3 then the universe is {0,1,-1}.
Русский
Если |R| ≤ 3, то множество элементов равно {0,1,−1}.
LaTeX
$$$|R| \le 3 \Rightarrow (univ_R) = \{0,1,-1\}$$$
Lean4
theorem univ_of_card_le_three (h : Fintype.card R ≤ 3) : (univ : Finset R) = {0, 1, -1} :=
by
refine (eq_of_subset_of_card_le (subset_univ _) ?_).symm
rcases lt_or_eq_of_le h with h | h
· apply card_le_card
rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]
intro a ha
simp only [mem_insert, mem_singleton] at ha
rcases ha with rfl | rfl <;> simp
· have : Nontrivial R := by
refine Fintype.one_lt_card_iff_nontrivial.1 ?_
rw [h]
simp
rw [card_univ, h, card_insert_of_notMem, card_insert_of_notMem, card_singleton]
· rw [mem_singleton]
intro H
rw [← add_eq_zero_iff_eq_neg, one_add_one_eq_two] at H
apply_fun (ringEquivOfPrime R Nat.prime_three h).symm at H
simp only [map_ofNat, map_zero] at H
replace H : ((2 : ℕ) : ZMod 3) = 0 := H
rw [natCast_eq_zero_iff] at H
norm_num at H
· intro h
simp only [mem_insert, mem_singleton, zero_eq_neg] at h
rcases h with (h | h)
· exact zero_ne_one h
· exact zero_ne_one h.symm
