English
In ZMod 2, the group of units is a singleton.
Русский
В ZMod 2 группа единиц является синглитоном.
LaTeX
$$Subsingleton (Units (ZMod 2))$$
Lean4
theorem neg_eq_self_iff {n : ℕ} (a : ZMod n) : -a = a ↔ a = 0 ∨ 2 * a.val = n :=
by
rw [neg_eq_iff_add_eq_zero, ← two_mul]
cases n
· rw [@mul_eq_zero ℤ, @mul_eq_zero ℕ, val_eq_zero]
exact ⟨fun h => h.elim (by simp) Or.inl, fun h => Or.inr (h.elim id fun h => h.elim (by simp) id)⟩
conv_lhs => rw [← a.natCast_zmod_val, ← Nat.cast_two, ← Nat.cast_mul, natCast_eq_zero_iff]
constructor
· rintro ⟨m, he⟩
rcases m with - | m
· rw [mul_zero, mul_eq_zero] at he
rcases he with (⟨⟨⟩⟩ | he)
exact Or.inl (a.val_eq_zero.1 he)
cases m
· right
rwa [show 0 + 1 = 1 from rfl, mul_one] at he
refine (a.val_lt.not_ge <| Nat.le_of_mul_le_mul_left ?_ zero_lt_two).elim
rw [he, mul_comm]
apply Nat.mul_le_mul_left
simp
· rintro (rfl | h)
· rw [val_zero, mul_zero]
apply dvd_zero
· rw [h]
