English
For any d dividing |α|, the number of elements of α of order d equals φ(d).
Русский
Для каждого d, делящего |α|, число элементов α порядка d равно φ(d).
LaTeX
$$#{a : α | orderOf a = d} = φ(d)$$
Lean4
@[to_additive]
theorem card_orderOf_eq_totient_aux₂ {d : ℕ} (hd : d ∣ Fintype.card α) : #{a : α | orderOf a = d} = φ d :=
by
let c := Fintype.card α
have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
apply card_orderOf_eq_totient_aux₁ hn hd
by_contra h0
simp_rw [not_lt, Nat.le_zero, Finset.card_eq_zero] at h0
apply lt_irrefl c
calc
c = ∑ m ∈ c.divisors, #{a : α | orderOf a = m} :=
by
simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
apply congr_arg card
simp [c]
_ = ∑ m ∈ c.divisors.erase d, #{a : α | orderOf a = m} :=
by
rw [eq_comm]
refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_
have : m = d := by
contrapose! hm₂
exact mem_erase_of_ne_of_mem hm₂ hm₁
simp [this, h0]
_ ≤ ∑ m ∈ c.divisors.erase d, φ m := by
refine sum_le_sum fun m hm => ?_
have hmc : m ∣ c := by
simp only [mem_erase, mem_divisors] at hm
tauto
obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
· simp [h1]
· simp [card_orderOf_eq_totient_aux₁ hn hmc h1]
_ < ∑ m ∈ c.divisors, φ m :=
(sum_erase_lt_of_pos (mem_divisors.2 ⟨hd, hc0.ne'⟩) (totient_pos.2 (pos_of_dvd_of_pos hd hc0)))
_ = c := sum_totient _
