ClassEquation

📁 Source: Mathlib/GroupTheory/ClassEquation.lean

Statistics

Metric	Count
Definitions	0
Theorems card_center_add_sum_card_noncenter_eq_card, nat_card_center_add_sum_card_noncenter_eq_card, sum_card_conj_classes_eq_card, sum_conjClasses_card_eq_card	4
Total	4

Group

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_center_add_sum_card_noncenter_eq_card 📖	mathematical	—	Fintype.card Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.center Finset.sum ConjClasses DivInvMonoid.toMonoid toDivInvMonoid Nat.instAddCommMonoid Set.toFinset ConjClasses.noncenter Finset.card ConjClasses.carrier	—	Nat.card_eq_fintype_card finsum_set_coe_eq_finsum_mem finsum_eq_sum_of_fintype Finset.sum_set_coe Finset.sum_congr Set.toFinset_card nat_card_center_add_sum_card_noncenter_eq_card Finite.of_fintype
nat_card_center_add_sum_card_noncenter_eq_card 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.center finsum ConjClasses DivInvMonoid.toMonoid toDivInvMonoid Nat.instAddCommMonoid Set Set.instMembership ConjClasses.noncenter Set.Elem ConjClasses.carrier	—	nonempty_fintype Nat.card_eq_fintype_card sum_conjClasses_card_eq_card Finset.sum_sdiff Finset.subset_univ finsum_congr_Prop Finset.sum_congr Set.toFinset_card Fintype.card_congr ConjClasses.mk_bijOn Set.toFinset_compl Finset.compl_eq_univ_sdiff Finset.card_eq_sum_ones Finset.card_eq_one Finset.coe_injective Set.coe_toFinset Finset.coe_singleton Set.Subsingleton.eq_singleton_of_mem Set.toFinset_setOf finsum_cond_eq_sum_of_cond_iff
sum_card_conj_classes_eq_card 📖	mathematical	—	finsum ConjClasses DivInvMonoid.toMonoid toDivInvMonoid Nat.instAddCommMonoid Set.ncard ConjClasses.carrier Nat.card	—	nonempty_fintype Nat.card_eq_fintype_card sum_conjClasses_card_eq_card finsum_eq_sum_of_fintype Finset.sum_congr Set.ncard_eq_toFinset_card' Set.toFinset_card

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sum_conjClasses_card_eq_card 📖	mathematical	—	Finset.sum ConjClasses DivInvMonoid.toMonoid Group.toDivInvMonoid Nat.instAddCommMonoid Finset.univ Finset.card Set.toFinset ConjClasses.carrier Fintype.card	—	Finset.sum_congr Set.toFinset_card Fintype.card_sigma Fintype.card_congr

---

← Back to Index