English
If p is an odd prime, then the unit group (Z/(p^n)Z)× is cyclic for all n.
Русский
Если p — нечетное простое, то группа единиц Z/(p^n)Z циклична для всех n.
LaTeX
$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\text{Prime}(p), \\\\text{p odd} \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, IsCyclic\\\\left((\\\\mathbb{Z}/p^{n}\\\\mathbb{Z})^{\\\\times}\\\\right).$$$$
Lean4
/-- If `p` is an odd prime, then `(ZMod (p ^ n))ˣ` is cyclic for all n -/
theorem isCyclic_units_of_prime_pow (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (n : ℕ) : IsCyclic (ZMod (p ^ n))ˣ :=
by
have _ : NeZero (p ^ n) := ⟨pow_ne_zero n hp.ne_zero⟩
have := Fact.mk hp
rcases n with _ | n
· rw [pow_zero];
infer_instance
-- We first consider the element `1 + p` of order `p ^ n`
set a := (1 + p : ZMod (p ^ (n + 1))) with ha_def
have ha : IsUnit a :=
by
rw [ha_def, ← Nat.cast_one (R := ZMod _), ← Nat.cast_add, ZMod.isUnit_iff_coprime]
apply Nat.Coprime.pow_right
simp only [Nat.coprime_add_self_left, Nat.coprime_one_left_eq_true]
have ha' : orderOf ha.unit = p ^ n :=
by
rw [← orderOf_injective _ Units.coeHom_injective ha.unit, Units.coeHom_apply, IsUnit.unit_spec]
exact orderOf_one_add_prime hp hp2 n
obtain ⟨c, hc⟩ := isCyclic_iff_exists_orderOf_eq_natCard.mp (isCyclic_units_prime hp)
rw [Nat.card_eq_fintype_card, ZMod.card_units] at hc
obtain ⟨(b : (ZMod (p ^ (n + 1)))ˣ), rfl⟩ := ZMod.unitsMap_surjective (Dvd.intro_left (p ^ n) rfl) c
have : p - 1 ∣ orderOf b := hc ▸ orderOf_map_dvd _ b
let k := orderOf b / (p - 1)
have : orderOf (b ^ k) = p - 1 := orderOf_pow_orderOf_div (orderOf_pos b).ne' this
rw [isCyclic_iff_exists_orderOf_eq_natCard]
-- The product of `ha.unit` and `b ^ k` has the required order
use ha.unit * b ^ k
rw [(Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime, this, Nat.card_eq_fintype_card,
ZMod.card_units_eq_totient, Nat.totient_prime_pow_succ hp, ← ha']
rw [ha', this]
apply Nat.Coprime.pow_left
rw [Nat.coprime_self_sub_right hp.pos]
simp
