Rank

📁 Source: Mathlib/GroupTheory/Rank.lean

Statistics

Metric	Count
Definitions rank, rank	2
Theorems rank_congr, rank_le, rank_le_of_surjective, rank_range_le, rank_spec, rank_closure_finite_le_nat_card, rank_closure_finset_le_card, rank_congr, rank_congr, rank_le, rank_le_of_surjective, rank_range_le, rank_spec, nat_card_centralizer_nat_card_stabilizer, rank_closure_finite_le_nat_card, rank_closure_finset_le_card, rank_congr	17
Total	19

AddGroup

Definitions

Name	Category	Theorems
rank 📖	CompOp	10 math math: rank_le, AddSubgroup.rank_closure_finset_le_card, AddSubgroup.rank_closure_finite_le_nat_card, rank_spec, rank_congr, card_dvd_exponent_nsmul_rank, rank_le_of_surjective, card_dvd_exponent_nsmul_rank', rank_range_le, AddSubgroup.rank_congr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_congr 📖	mathematical	—	rank	—	le_antisymm rank_le_of_surjective AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddEquiv.surjective
rank_le 📖	mathematical	AddSubgroup.closure SetLike.coe Finset Finset.instSetLike Top.top AddSubgroup AddSubgroup.instTop	rank Finset.card	—	Nat.find_le fg_iff'
rank_le_of_surjective 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid toSubNegMonoid AddMonoidHom.instFunLike	rank	—	rank_spec rank_le Finset.coe_image AddMonoidHom.map_closure AddSubgroup.map_top_of_surjective LE.le.trans_eq Finset.card_image_le
rank_range_le 📖	mathematical	—	rank AddSubgroup SetLike.instMembership AddSubgroup.instSetLike AddMonoidHom.range AddSubgroup.toAddGroup fg_range	—	rank_le_of_surjective fg_range AddMonoidHom.rangeRestrict_surjective
rank_spec 📖	mathematical	—	Finset.card rank AddSubgroup.closure SetLike.coe Finset Finset.instSetLike Top.top AddSubgroup AddSubgroup.instTop	—	Nat.find_spec fg_iff'

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_closure_finite_le_nat_card 📖	mathematical	—	AddGroup.rank AddSubgroup SetLike.instMembership instSetLike closure toAddGroup AddGroup.closure_finite_fg Nat.card Set.Elem	—	AddGroup.closure_finite_fg Nat.card_eq_fintype_card Set.toFinset_card AddGroup.closure_finset_fg rank_congr Set.coe_toFinset rank_closure_finset_le_card
rank_closure_finset_le_card 📖	mathematical	—	AddGroup.rank AddSubgroup SetLike.instMembership instSetLike closure SetLike.coe Finset Finset.instSetLike toAddGroup AddGroup.closure_finset_fg Finset.card	—	Function.Injective.injOn Subtype.coe_injective Finset.coe_preimage closure_preimage_eq_top LE.le.trans AddGroup.closure_finset_fg AddGroup.rank_le Finset.card_image_of_injOn Finset.image_preimage Finset.card_filter_le
rank_congr 📖	mathematical	—	AddGroup.rank AddSubgroup SetLike.instMembership instSetLike toAddGroup	—	—

Group

Definitions

Name	Category	Theorems
rank 📖	CompOp	14 math math: Subgroup.index_center_le_pow, card_dvd_exponent_pow_rank, Subgroup.rank_closure_finite_le_nat_card, rank_le_of_surjective, Subgroup.rank_congr, Subgroup.rank_le_index_mul_rank, rank_le, rank_spec, Subgroup.rank_commutator_le_card, Subgroup.rank_closure_finset_le_card, card_dvd_exponent_pow_rank', rank_range_le, rank_congr, rank_closureCommutatorRepresentatives_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_congr 📖	mathematical	—	rank	—	le_antisymm rank_le_of_surjective MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass MulEquiv.surjective
rank_le 📖	mathematical	Subgroup.closure SetLike.coe Finset Finset.instSetLike Top.top Subgroup Subgroup.instTop	rank Finset.card	—	Nat.find_le fg_iff'
rank_le_of_surjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid toDivInvMonoid MonoidHom.instFunLike	rank	—	rank_spec rank_le Finset.coe_image MonoidHom.map_closure Subgroup.map_top_of_surjective LE.le.trans_eq Finset.card_image_le
rank_range_le 📖	mathematical	—	rank Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.range Subgroup.toGroup fg_range	—	rank_le_of_surjective fg_range MonoidHom.rangeRestrict_surjective
rank_spec 📖	mathematical	—	Finset.card rank Subgroup.closure SetLike.coe Finset Finset.instSetLike Top.top Subgroup Subgroup.instTop	—	Nat.find_spec fg_iff'

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nat_card_centralizer_nat_card_stabilizer 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership instSetLike centralizer Set Set.instSingletonSet ConjAct ConjAct.instGroup MulAction.stabilizer MulDistribMulAction.toMulAction DivInvMonoid.toMonoid Group.toDivInvMonoid ConjAct.instMulDistribMulAction	—	centralizer_eq_comap_stabilizer
rank_closure_finite_le_nat_card 📖	mathematical	—	Group.rank Subgroup SetLike.instMembership instSetLike closure toGroup Group.closure_finite_fg Nat.card Set.Elem	—	Group.closure_finite_fg Nat.card_eq_fintype_card Set.toFinset_card Group.closure_finset_fg rank_congr Set.coe_toFinset rank_closure_finset_le_card
rank_closure_finset_le_card 📖	mathematical	—	Group.rank Subgroup SetLike.instMembership instSetLike closure SetLike.coe Finset Finset.instSetLike toGroup Group.closure_finset_fg Finset.card	—	Function.Injective.injOn Subtype.coe_injective Finset.coe_preimage closure_preimage_eq_top LE.le.trans Group.closure_finset_fg Group.rank_le Finset.card_image_of_injOn Finset.image_preimage Finset.card_filter_le
rank_congr 📖	mathematical	—	Group.rank Subgroup SetLike.instMembership instSetLike toGroup	—	—

---

← Back to Index