sum_conjClasses_card_eq_card
theorem sum_conjClasses_card_eq_card :
∀ (G : Type u_1) [inst : Group G] [inst_1 : Fintype (ConjClasses G)] [inst_2 : Fintype G]
[inst_3 : (x : ConjClasses G) → Fintype ↑x.carrier],
(Finset.univ.sum fun x => x.carrier.toFinset.card) = Fintype.card G
This theorem states that in any finite group `G`, the sum of the cardinalities (i.e., the number of elements) of all its conjugacy classes is equal to the cardinality of the group itself. In other words, the conjugacy classes of a group form a partition of that group, such that every element of the group is in exactly one conjugacy class. This is a fundamental result in group theory, reflecting the structure of groups and their symmetry properties.
More concisely: In a finite group, the sum of the sizes of all its conjugacy classes equals the group's order.
|
Group.nat_card_center_add_sum_card_noncenter_eq_card
theorem Group.nat_card_center_add_sum_card_noncenter_eq_card :
∀ (G : Type u_1) [inst : Group G] [inst_1 : Finite G],
(Nat.card ↥(Subgroup.center G) + finsum fun x => finsum fun h => Nat.card ↑x.carrier) = Nat.card G
The theorem `Group.nat_card_center_add_sum_card_noncenter_eq_card` is known as the class equation for finite groups. It states that for any finite group `G`, the cardinality (or size) of the group is equal to the cardinality of its center plus the sum of the cardinalities of all its nontrivial conjugacy classes. In other words, the total number of elements in a group is distributed among its center and its nontrivial conjugacy classes. If `G` is the group, this can be represented mathematically as: `|G| = |Z(G)| + ∑ |Cl(x)|` for all x not in the center of the group. Here, `|Z(G)|` represents the size of the center of `G`, `Cl(x)` denotes the conjugacy class of an element `x`, and the summation `∑` runs over all `x` not in the center of the group.
More concisely: The cardinality of a finite group is equal to the sum of the cardinality of its center and the sum of the cardinalities of all its nontrivial conjugacy classes.
|
Group.sum_card_conj_classes_eq_card
theorem Group.sum_card_conj_classes_eq_card :
∀ (G : Type u_1) [inst : Group G] [inst_1 : Finite G], (finsum fun x => x.carrier.ncard) = Nat.card G
This theorem states that in any finite group G, the sum of the cardinalities (sizes) of all the conjugacy classes equals the cardinality of the group itself. In other words, if you add up the sizes of all these classes, you get the size of the whole group. This supports the interpretation that conjugacy classes partition the group in a sense that every element of the group belongs to exactly one conjugacy class, and therefore, there is no overlap or missing elements.
More concisely: The sum of the sizes of all conjugacy classes in a finite group equals the group's order.
|