CardCommute

📁 Source: Mathlib/GroupTheory/GroupAction/CardCommute.lean

Statistics

Metric	Count
Definitions	0
Theorems card_eq_sum_card_addGroup_sub_card_stabilizer, card_eq_sum_card_addGroup_sub_card_stabilizer', card_eq_sum_card_group_div_card_stabilizer, card_eq_sum_card_group_div_card_stabilizer', card_comm_eq_card_conjClasses_mul_card, instInfiniteProdSubtypeCommute	6
Total	6

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_sum_card_addGroup_sub_card_stabilizer 📖	mathematical	—	Fintype.card Finset.sum orbitRel Nat.instAddCommMonoid Finset.univ AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer Quotient.out	—	card_eq_sum_card_addGroup_sub_card_stabilizer' Quotient.out_eq'
card_eq_sum_card_addGroup_sub_card_stabilizer' 📖	mathematical	orbitRel Quotient.mk''	Fintype.card Finset.sum Nat.instAddCommMonoid Finset.univ AddSubgroup SetLike.instMembership AddSubgroup.instSetLike stabilizer	—	Fintype.card_congr Fintype.card_prod Fintype.card_pos_iff Zero.instNonempty Finset.sum_congr Fintype.card_sigma

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_sum_card_group_div_card_stabilizer 📖	mathematical	—	Fintype.card Finset.sum orbitRel Nat.instAddCommMonoid Finset.univ Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer Quotient.out	—	card_eq_sum_card_group_div_card_stabilizer' Quotient.out_eq'
card_eq_sum_card_group_div_card_stabilizer' 📖	mathematical	orbitRel Quotient.mk''	Fintype.card Finset.sum Nat.instAddCommMonoid Finset.univ Subgroup SetLike.instMembership Subgroup.instSetLike stabilizer	—	Fintype.card_congr Fintype.card_prod Fintype.card_pos_iff One.instNonempty Finset.sum_congr

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_comm_eq_card_conjClasses_mul_card 📖	mathematical	—	Nat.card Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid ConjClasses	—	Nat.card_eq_fintype_card Fintype.card_congr Fintype.card_sigma Fintype.sum_equiv Fintype.card_congr' mul_inv_eq_iff_eq_mul MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group Setoid.ext Setoid.comm' isConj_iff mul_comm Nat.card_eq_zero_of_infinite instInfiniteProdSubtypeCommute MulZeroClass.zero_mul
instInfiniteProdSubtypeCommute 📖	mathematical	—	Infinite Commute	—	Infinite.of_injective

---

← Back to Index