English
Cyclic property is preserved under multiplicative isomorphism.
Русский
Свойство цикличности сохраняется под мультипликативным изоморфизмом.
LaTeX
$$IsCyclic(G) ⇔ IsCyclic(G') for e : G ≃* G'$$
Lean4
@[to_additive IsAddCyclic.card_nsmul_eq_zero_le]
theorem card_pow_eq_one_le [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) : #{a : α | a ^ n = 1} ≤ n :=
let ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
calc
#{a : α | a ^ n = 1} ≤ #(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) : Set α).toFinset :=
card_le_card fun x hx =>
let ⟨m, hm⟩ := show x ∈ Submonoid.powers g from mem_powers_iff_mem_zpowers.2 <| hg x
Set.mem_toFinset.2
⟨(m / (Fintype.card α / Nat.gcd n (Fintype.card α)) : ℕ),
by
dsimp at hm
have hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1 := by rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff];
exact (mem_filter.1 hx).2
dsimp only
rw [zpow_natCast, ← pow_mul, Nat.mul_div_cancel_left', hm]
refine Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_
conv_lhs =>
rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card, ←
orderOf_eq_card_of_forall_mem_zpowers hg]
exact orderOf_dvd_of_pow_eq_one hgmn⟩
_ ≤ n := by
let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)
have hm0 : 0 < m :=
Nat.pos_of_ne_zero fun hm0 => by
rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
exact hm.elim' 1
simp only [Set.toFinset_card, SetLike.coe_sort_coe]
rw [Fintype.card_zpowers, orderOf_pow g, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
nth_rw 2 [hm]; nth_rw 3 [hm]
rw [Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left, hm, Nat.mul_div_cancel _ hm0]
exact le_of_dvd hn0 (Nat.gcd_dvd_left _ _)
