Counting the elements of a cyclic group by a condition on their order

In a finite cyclic group, the number of elements whose order satisfies a predicate p is the sum of φ d over the divisors d of the group order that satisfy p.

Mathlib counts elements of an exact order: IsCyclic.card_orderOf_eq_totient says there are φ d of them for each d dividing the group order. Summing that over the divisors selected by p is the whole content here.

The point of stating it for a predicate is that it turns a count defined by a condition on orders into an arithmetic sum over divisors, where the group has disappeared. Whatever p is, the answer is a totient sum over {d ∣ #α | p d}, so it can then be evaluated or estimated by number theory alone.

Main results

• IsCyclic.card_filter_orderOf_eq_sum_totient, and its additive counterpart: the count of elements whose order satisfies p is ∑ φ d over the divisors d of the group order with p d.
• IsCyclic.card_filter_dvd_orderOf_eq_sum_totient: the case p = (f ∣ ·).
• IsCyclic.card_filter_dvd_orderOf_mul_prod_primeFactors, and its additive counterpart: that case in closed form, in ℕ.
• IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors, and its additive counterpart: the closed form as a product over ℚ.
• IsCyclic.le_card_filter_dvd_orderOf, and its additive counterpart: the uniform lower bound (1 - 2 ^ -r) ^ #f.primeFactors for the proportion of elements of order divisible by f, when f ^ r ∣ #α.

The elements of order divisible by f, in closed form

Let α have order h and let f divide h. The elements of α whose order is a multiple of f are counted exactly:

#{τ | f ∣ orderOf τ} = h * ∏ p ∣ f, (1 - p ^ -(v_p h - v_p f + 1)),

the product running over the primes of f. Writing τ = g ^ k for a generator g, f divides the order of τ exactly when p ^ (v_p h - v_p f + 1) fails to divide k for every prime p of f (IsOfFinOrder.dvd_orderOf_pow_iff). Those conditions constrain k modulo coprime prime powers, so they are independent and the count is a product.

Two forms of the count are recorded: an identity in ℕ, cleared of denominators, and the displayed product over ℚ. At f = h every exponent is 1 and the count becomes Euler's product formula Nat.totient_mul_prod_primeFactors, since the elements whose order is a multiple of h are the φ h generators.

The third result is the estimate that makes the count usable when f is fixed and h is divisible by a high power of f: if f ^ r ∣ h with 1 ≤ r, every factor of the product is at least 1 - 2 ^ -r, so the proportion of elements of order divisible by f is at least (1 - 2 ^ -r) ^ #f.primeFactors, which tends to 1 as r grows.

theorem IsCyclic.card_filter_orderOf_eq_sum_totient {α : Type u_1} [Group α] [Fintype α] [IsCyclic α] (p : ℕ → Prop) [DecidablePred p] : {τ : α | p (orderOf τ)}.card = ∑ d ∈ (Fintype.card α).divisors with p d, d.totient

The elements of a cyclic group whose order satisfies p, counted by order. Each divisor d of the group order contributes its φ d elements of order exactly d, and the condition p (orderOf τ) keeps precisely the divisors satisfying p.

theorem IsAddCyclic.card_filter_addOrderOf_eq_sum_totient {α : Type u_1} [AddGroup α] [Fintype α] [IsAddCyclic α] (p : ℕ → Prop) [DecidablePred p] : {τ : α | p (addOrderOf τ)}.card = ∑ d ∈ (Fintype.card α).divisors with p d, d.totient

The elements of a finite additive cyclic group whose order satisfies p, counted by order. Each divisor d of the group order contributes its φ d elements of addOrderOf exactly d, and the condition p (addOrderOf τ) keeps precisely the divisors satisfying p.

theorem IsCyclic.card_filter_dvd_orderOf_eq_sum_totient {α : Type u_1} [Group α] [Fintype α] [IsCyclic α] (f : ℕ) : {τ : α | f ∣ orderOf τ}.card = ∑ d ∈ (Fintype.card α).divisors with f ∣ d, d.totient

The elements of a cyclic group whose order is a multiple of f, counted by order. The divisibility case of IsCyclic.card_filter_orderOf_eq_sum_totient.

theorem IsAddCyclic.card_filter_dvd_addOrderOf_eq_sum_totient {α : Type u_1} [AddGroup α] [Fintype α] [IsAddCyclic α] (f : ℕ) : {τ : α | f ∣ addOrderOf τ}.card = ∑ d ∈ (Fintype.card α).divisors with f ∣ d, d.totient

The elements of a finite additive cyclic group whose order is a multiple of f, counted by order. The divisibility case of IsAddCyclic.card_filter_addOrderOf_eq_sum_totient.

theorem IsCyclic.card_filter_dvd_orderOf_mul_prod_primeFactors {α : Type u_1} [Group α] [Fintype α] [IsCyclic α] {f : ℕ} (hf : f ∣ Fintype.card α) : {τ : α | f ∣ orderOf τ}.card * ∏ p ∈ f.primeFactors, p ^ ((Fintype.card α).factorization p - f.factorization p + 1) = Fintype.card α * ∏ p ∈ f.primeFactors, (p ^ ((Fintype.card α).factorization p - f.factorization p + 1) - 1)

The number of elements of a cyclic group whose order is a multiple of f. For f dividing the order h of a cyclic group, the elements of order divisible by f number h * ∏ p ∣ f, (1 - p ^ -(v_p h - v_p f + 1)), stated here cleared of denominators.

At f = h every exponent is 1 and this is Euler's product formula Nat.totient_mul_prod_primeFactors, the elements of order divisible by h being the φ h generators.

theorem IsAddCyclic.card_filter_dvd_addOrderOf_add_sum_primeFactors {α : Type u_1} [AddGroup α] [Fintype α] [IsAddCyclic α] {f : ℕ} (hf : f ∣ Fintype.card α) : {τ : α | f ∣ addOrderOf τ}.card * ∏ p ∈ f.primeFactors, p ^ ((Fintype.card α).factorization p - f.factorization p + 1) = Fintype.card α * ∏ p ∈ f.primeFactors, (p ^ ((Fintype.card α).factorization p - f.factorization p + 1) - 1)

The number of elements of an additive cyclic group whose additive order is a multiple of f. This is the additive counterpart of IsCyclic.card_filter_dvd_orderOf_mul_prod_primeFactors.

theorem IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors {α : Type u_1} [Group α] [Fintype α] [IsCyclic α] {f : ℕ} (hf : f ∣ Fintype.card α) : ↑{τ : α | f ∣ orderOf τ}.card = ↑(Fintype.card α) * ∏ p ∈ f.primeFactors, (1 - (↑p ^ ((Fintype.card α).factorization p - f.factorization p + 1))⁻¹)

Euler's product formula for the elements of order divisible by f. For f dividing the order h of a cyclic group, the elements of order divisible by f are a proportion ∏ p ∣ f, (1 - p ^ -(v_p h - v_p f + 1)) of the group, the product running over the primes of f.

theorem IsAddCyclic.card_filter_dvd_addOrderOf_eq_add_sum_primeFactors {α : Type u_1} [AddGroup α] [Fintype α] [IsAddCyclic α] {f : ℕ} (hf : f ∣ Fintype.card α) : ↑{τ : α | f ∣ addOrderOf τ}.card = ↑(Fintype.card α) * ∏ p ∈ f.primeFactors, (1 - (↑p ^ ((Fintype.card α).factorization p - f.factorization p + 1))⁻¹)

Euler's product formula for the elements of additive order divisible by f. This is the additive counterpart of IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors.

theorem IsCyclic.le_card_filter_dvd_orderOf {α : Type u_1} [Group α] [Fintype α] [IsCyclic α] {f r : ℕ} (hr : 1 ≤ r) (hfr : f ^ r ∣ Fintype.card α) : (1 - 2⁻¹ ^ r) ^ f.primeFactors.card * ↑(Fintype.card α) ≤ ↑{τ : α | f ∣ orderOf τ}.card

A uniform lower bound for the elements of order divisible by f. If the order of the cyclic group is divisible by f ^ r with 1 ≤ r, then at least a proportion (1 - 2 ^ -r) ^ #f.primeFactors of its elements have order divisible by f.

Each factor of card_filter_dvd_orderOf_eq_mul_prod_primeFactors is bounded below by 1 - 2 ^ -r because f ^ r ∣ h forces the exponent v_p h - v_p f + 1 to be at least r at every prime p of f, and p is at least 2. The bound depends on f only through its number of prime factors, so it tends to 1 as r grows.

theorem IsAddCyclic.le_card_filter_dvd_addOrderOf {α : Type u_1} [AddGroup α] [Fintype α] [IsAddCyclic α] {f r : ℕ} (hr : 1 ≤ r) (hfr : f ^ r ∣ Fintype.card α) : (1 - 2⁻¹ ^ r) ^ f.primeFactors.card * ↑(Fintype.card α) ≤ ↑{τ : α | f ∣ addOrderOf τ}.card

A uniform lower bound for the elements of additive order divisible by f. This is the additive counterpart of IsCyclic.le_card_filter_dvd_orderOf.