English
The unit group (ZMod n)× is cyclic iff n is 0, 1, 2, 4 or n = p^m or n = 2 p^m with p odd prime and m ≥ 1.
Русский
Группа единиц (ZMod n)× циклична тогда и только тогда, когда n имеет форму 0, 1, 2, 4 или n = p^m или n = 2 p^m с нечетным простым p и m ≥ 1.
LaTeX
$$$\\\\IsCyclic\\\\left((\\\\mathbb{Z}/n\\\\mathbb{Z})^{\\\\times}\\\\right) \\\\Leftrightarrow n = 0 \\\\lor n = 1 \\\\lor n = 2 \\\\lor n = 4 \\\\lor \\\\\\exists p,m: p\\\\Prime \\\\land Odd(p) \\\\land 1 \\\\le m \\\\land (n = p^{m} \\\\lor n = 2 p^{m}).$$$$
Lean4
/-- `(ZMod n)ˣ` is cyclic iff `n` is of the form
`0`, `1`, `2`, `4`, `p ^ m`, or `2 * p ^ m`,
where `p` is an odd prime and `1 ≤ m`. -/
theorem isCyclic_units_iff (n : ℕ) :
IsCyclic (ZMod n)ˣ ↔
n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ (p m : ℕ), p.Prime ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m) :=
by
by_cases h0 : n = 0
· rw [h0]; simp [isCyclic_units_zero]
by_cases h1 : n = 1
· rw [h1]; simp [isCyclic_units_one]
by_cases h2 : n = 2
· rw [h2]; simp [isCyclic_units_two]
by_cases h4 : n = 4
· rw [h4]; simp [isCyclic_units_four]
simp only [h0, h1, h2, h4, false_or, and_or_left, exists_or]
rcases (n.even_or_odd).symm with hn | hn
· rw [isCyclic_units_iff_of_odd hn, or_iff_left]
· congr! with p m
rw [and_iff_right_of_imp]
rintro rfl
contrapose! h1
cases Nat.lt_one_iff.mp h1
apply pow_zero
· rintro ⟨p, m, -, -, -, rfl⟩
simp [← Nat.not_even_iff_odd] at hn
obtain ⟨n, rfl⟩ := hn.two_dvd
rcases (n.even_or_odd).symm with hn | hn
· rw [isCyclic_units_two_mul_iff_of_odd _ hn, isCyclic_units_iff_of_odd hn, or_iff_right]
· congr! with p m
rw [Nat.mul_left_cancel_iff zero_lt_two, and_iff_right_of_imp]
rintro rfl
contrapose! h2
cases Nat.lt_one_iff.mp h2
rw [pow_zero, mul_one]
· rintro ⟨p, m, -, odd, -, eq⟩
have := eq ▸ odd.pow
simp [← Nat.not_even_iff_odd] at this
obtain ⟨n, rfl⟩ := hn.two_dvd
apply iff_of_false
· rw [← mul_assoc, show 2 * 2 = 4 from rfl, isCyclic_units_four_mul_iff]
cutsat
grind
