sum_card_orderOf_eq_card_pow_eq_one

English

In a finite group, the sum over divisors of order computes a cardinal equality involving powers and finiteness.

Русский

В конечной группе сумма по делителям порядка даёт кардинальное равенство, связанное с степенями и конечностью.

LaTeX

$$sum_card_orderOf_eq_card_pow_eq_one$$

Lean4

@[to_additive]
theorem sum_card_orderOf_eq_card_pow_eq_one [Fintype G] [DecidableEq G] (hn : n ≠ 0) :
    ∑ m ∈ divisors n, #{x : G | orderOf x = m} = #{x : G | x ^ n = 1} :=
  by
  refine (Finset.card_biUnion ?_).symm.trans ?_
  · simp +contextual [Set.PairwiseDisjoint, Set.Pairwise, disjoint_iff, Finset.ext_iff]
  · congr; ext; simp [hn, orderOf_dvd_iff_pow_eq_one]

Похожие утверждения