Finite

📁 Source: Mathlib/GroupTheory/Commutator/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems commutator_pi_pi_of_finite, finiteIndex_center, index_center_le_pow, instFGSubtypeMemCommutator, rank_commutator_le_card, card_commutatorSet_closureCommutatorRepresentatives, card_commutator_closureCommutatorRepresentatives, closureCommutatorRepresentatives_fg, instFiniteElemProdCommutatorRepresentatives, instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet, rank_closureCommutatorRepresentatives_le	11
Total	11

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutator_pi_pi_of_finite 📖	mathematical	—	Bracket.bracket Subgroup Pi.group commutator pi Set.univ	—	le_antisymm commutator_pi_pi_le pi_le_iff map_commutator commutator_mono le_pi_iff Pi.mulSingle_eq_same Pi.mulSingle_eq_of_ne SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass instSubgroupClass
finiteIndex_center 📖	mathematical	—	FiniteIndex center	—	Group.rank_spec Finite.card_eq_zero_of_embedding LT.lt.ne' Finite.card_pos Pi.finite Finite.of_fintype instNonemptyElemCommutatorSet
index_center_le_pow 📖	mathematical	—	index center Monoid.toNatPow Nat.instMonoid Nat.card Set.Elem commutatorSet Group.rank	—	Group.rank_spec Fintype.card_coe Nat.card_eq_fintype_card Finset.coe_sort_coe Nat.card_fun Finite.of_fintype Finite.card_le_of_embedding Pi.finite
instFGSubtypeMemCommutator 📖	mathematical	—	Group.FG Subgroup SetLike.instMembership instSetLike commutator toGroup	—	commutator_eq_closure Group.closure_finite_fg
rank_commutator_le_card 📖	mathematical	—	Group.rank Subgroup SetLike.instMembership instSetLike commutator toGroup instFGSubtypeMemCommutator Nat.card Set.Elem commutatorSet	—	instFGSubtypeMemCommutator Group.closure_finite_fg rank_congr commutator_eq_closure rank_closure_finite_le_nat_card

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_commutatorSet_closureCommutatorRepresentatives 📖	mathematical	—	Nat.card Set.Elem Subgroup SetLike.instMembership Subgroup.instSetLike closureCommutatorRepresentatives commutatorSet Subgroup.toGroup	—	image_commutatorSet_closureCommutatorRepresentatives Nat.card_congr Subgroup.subtype_injective
card_commutator_closureCommutatorRepresentatives 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike closureCommutatorRepresentatives Subgroup.toGroup commutator	—	commutator_eq_closure image_commutatorSet_closureCommutatorRepresentatives MonoidHom.map_closure Nat.card_congr Subgroup.subtype_injective
closureCommutatorRepresentatives_fg 📖	mathematical	—	Group.FG Subgroup SetLike.instMembership Subgroup.instSetLike closureCommutatorRepresentatives Subgroup.toGroup	—	Group.closure_finite_fg Finite.Set.finite_union Finite.Set.finite_image instFiniteElemProdCommutatorRepresentatives
instFiniteElemProdCommutatorRepresentatives 📖	mathematical	—	Finite Set.Elem commutatorRepresentatives	—	Set.finite_coe_iff Set.finite_range
instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet 📖	mathematical	—	Finite Set.Elem Subgroup SetLike.instMembership Subgroup.instSetLike closureCommutatorRepresentatives commutatorSet Subgroup.toGroup	—	Nat.finite_of_card_ne_zero card_commutatorSet_closureCommutatorRepresentatives LT.lt.ne' Finite.card_pos instNonemptyElemCommutatorSet
rank_closureCommutatorRepresentatives_le 📖	mathematical	—	Group.rank Subgroup SetLike.instMembership Subgroup.instSetLike closureCommutatorRepresentatives Subgroup.toGroup closureCommutatorRepresentatives_fg Nat.card Set.Elem commutatorSet	—	closureCommutatorRepresentatives_fg Nat.instAtLeastTwoHAddOfNat two_mul LE.le.trans Group.closure_finite_fg Finite.Set.finite_union Finite.Set.finite_image instFiniteElemProdCommutatorRepresentatives Subgroup.rank_closure_finite_le_nat_card Set.card_union_le add_le_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finite.card_image_le Finite.card_range_le

---

← Back to Index