card_center_add_sum_card_noncenter_eq_card

English

In a finite group G, the order of the center plus the sum of the sizes of noncentral conjugacy classes equals the order of G.

Русский

В конечной группе G сумма по размеру центра и по размерам некцентральных классов равна порядку G.

LaTeX

$$$|Z(G)| + \\sum_{C \\in \\mathrm{noncenter}(G).toFinset} |C| = |G|$$$

Lean4

theorem card_center_add_sum_card_noncenter_eq_card (G) [Group G] [∀ x : ConjClasses G, Fintype x.carrier] [Fintype G]
    [Fintype <| Subgroup.center G] [Fintype <| noncenter G] :
    Fintype.card (Subgroup.center G) + ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G :=
  by
  convert Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2
  · simp
  · rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype, ← Finset.sum_set_coe]
    simp
  · simp

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