English
If m and n are odd, >1, coprime, then (ZMod(mn))× is not cyclic.
Русский
Если m и n — четные? Нет, нечетные больше 1 и взаимно просты, то (ZMod(mn))× не циклична.
LaTeX
$$$\\\\text{If } m,n \\\\text{ are odd } m>1, n>1, \\\\ gcd(m,n)=1, \\\\Rightarrow \\\\neg IsCyclic\\\\left((\\\\mathbb{Z}/(mn)\\\\mathbb{Z})^{\\\\times}\\\\right).$$$$
Lean4
theorem not_isCyclic_units_of_mul_coprime (m n : ℕ) (hm : Odd m) (hm1 : m ≠ 1) (hn : Odd n) (hn1 : n ≠ 1)
(hmn : m.Coprime n) : ¬IsCyclic (ZMod (m * n))ˣ := by
classical
have _ : NeZero m := ⟨Nat.ne_of_odd_add hm⟩
have _ : NeZero n := ⟨Nat.ne_of_odd_add hn⟩
let e := (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans .prodUnits
rw [e.isCyclic, Group.isCyclic_prod_iff]
rintro ⟨-, -, h⟩
simp_rw [Nat.card_eq_fintype_card, card_units_eq_totient, Nat.totient_coprime_totient_iff, hm1, hn1, false_or] at h
rcases h with (rfl | rfl)
· simp [← Nat.not_even_iff_odd] at hm
· simp [← Nat.not_even_iff_odd] at hn
