English
As an equivalent formulation, the number of order-n points equals φ(n).
Русский
Альтернативная формулировка: число точек порядка n равно φ(n).
LaTeX
$$Nat.card{u: AddCircle(p) // addOrderOf(u) = n} = totient(n)$$
Lean4
@[simp]
theorem card_addOrderOf_eq_totient {n : ℕ} : Nat.card { u : AddCircle p // addOrderOf u = n } = n.totient :=
by
rcases n.eq_zero_or_pos with (rfl | hn)
· simp only [Nat.totient_zero, addOrderOf_eq_zero_iff]
rcases em (∃ u : AddCircle p, ¬IsOfFinAddOrder u) with (⟨u, hu⟩ | h)
· have : Infinite { u : AddCircle p // ¬IsOfFinAddOrder u } :=
by
rw [← coe_setOf, infinite_coe_iff]
exact infinite_not_isOfFinAddOrder hu
exact Nat.card_eq_zero_of_infinite
· have : IsEmpty { u : AddCircle p // ¬IsOfFinAddOrder u } := by simpa [isEmpty_subtype] using h
exact Nat.card_of_isEmpty
· rw [← coe_setOf, Nat.card_congr (setAddOrderOfEquiv p hn), n.totient_eq_card_lt_and_coprime]
simp only [Nat.gcd_comm]
