English
Let n = p^k with p prime. For a ∈ ZMod n, if ord(a) is coprime to n, then either a = 1 or a − 1 is a unit modulo n.
Русский
Пусть n = p^k, p — простое. Для a ∈ ZMod n, если ord(a)coprime к n, то либо a = 1, либо a − 1 — единичный элемент по модулю n.
LaTeX
$$$\\\\forall n,p,k \\\\in \\\\mathbb{N}, \\\\text{p prime}, \\\\text{hn}: n = p^{k} \\\\Rightarrow \\\\forall a \\\\in ZMod(n), (\\\\operatorname{ord}(a)).\\\\text{Coprime}\\\\(n) \\\\Rightarrow (a = 1) \\\\lor \\\\text{IsUnit}(a-1)$$$
Lean4
theorem eq_one_or_isUnit_sub_one {n p k : ℕ} [Fact p.Prime] (hn : n = p ^ k) (a : ZMod n) (ha : (orderOf a).Coprime n) :
a = 1 ∨ IsUnit (a - 1) := by
rcases eq_or_ne n 0 with rfl | hn0
· exact Or.inl (orderOf_eq_one_iff.mp ((orderOf a).coprime_zero_right.mp ha))
rcases eq_or_ne a 0 with rfl | ha0
· exact Or.inr (zero_sub (1 : ZMod n) ▸ isUnit_neg_one)
have : NeZero n := ⟨hn0⟩
obtain ⟨a, rfl⟩ := ZMod.natCast_zmod_surjective a
rw [← orderOf_eq_one_iff, or_iff_not_imp_right]
refine fun h ↦ ha.eq_one_of_dvd ?_
rw [orderOf_dvd_iff_pow_eq_one, ← Nat.cast_pow, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff, hn]
replace ha0 : 1 ≤ a := by
contrapose! ha0
rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]
rw [← Nat.cast_one, ← Nat.cast_sub ha0, ZMod.isUnit_iff_coprime, hn] at h
obtain ⟨b, hb⟩ := not_imp_comm.mp (Nat.Prime.coprime_pow_of_not_dvd Fact.out) h
rw [tsub_eq_iff_eq_add_of_le ha0, add_comm] at hb
exact hb ▸ pow_pow_modEq_one p k b
