English
For odd n, IsCyclic((ZMod n)×) holds iff n is of the form 0, 1, 2, 4, or n = p^m or n = 2 p^m with p an odd prime and m ≥ 1.
Русский
Для нечетного n условие цикличности (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\\\\Pr\ime \\\\in \\\\mathbb{N}, \\\\Odd(p) \\\\land 1 \\\\le m \\\\land (n = p^{m} \\\\lor n = 2 p^{m}).$$$$
Lean4
theorem isCyclic_units_iff_of_odd {n : ℕ} (hn : Odd n) :
IsCyclic (ZMod n)ˣ ↔ ∃ (p m : ℕ), p.Prime ∧ Odd p ∧ n = p ^ m :=
by
have hn0 : n ≠ 0 := by rintro rfl; exact Nat.not_odd_zero hn
obtain rfl | h1 := eq_or_ne n 1
· simp_rw [isCyclic_units_one, true_iff]
exact ⟨3, 0, Nat.prime_three, by simp [Nat.odd_iff], by rw [pow_zero]⟩
have ⟨p, hp, dvd⟩ := n.exists_prime_and_dvd h1
have odd := hn.of_dvd_nat dvd
by_cases hnp : n = p ^ n.factorization p
· exact hnp ▸ iff_of_true (isCyclic_units_of_prime_pow p hp (odd.ne_two_of_dvd_nat dvd_rfl) _) ⟨p, _, hp, odd, rfl⟩
refine iff_of_false ?_ (mt ?_ hnp)
· have := n.ordProj_dvd p
rw [← Nat.mul_div_cancel' this]
refine
not_isCyclic_units_of_mul_coprime _ _ (hn.of_dvd_nat this) ?_ (hn.of_dvd_nat (Nat.div_dvd_of_dvd this)) ?_
((Nat.coprime_ordCompl hp hn0).pow_left ..)
· simpa only [Ne, pow_eq_one_iff (hp.factorization_pos_of_dvd hn0 dvd).ne'] using hp.ne_one
· contrapose! hnp
conv_lhs => rw [← Nat.div_mul_cancel this, hnp, one_mul]
rintro ⟨q, m, hq, -, rfl⟩
cases (Nat.prime_dvd_prime_iff_eq hp hq).mp (hp.dvd_of_dvd_pow dvd)
simp [hp.factorization_self] at hnp
