Finite

📁 Source: Mathlib/Algebra/Group/Subgroup/Finite.lean

Statistics

Metric	Count
Definitions `decidableMemRange`, `fintypeMrange`, `fintypeRange`, `fintypeBot`, `instFintypeSubtypeMemOfDecidablePred`, `decidableMemRange`, `fintypeMrange`, `fintypeRange`, `fintypeBot`, `instFintypeSubtypeMemOfDecidablePred`	10
Theorems `card_bot`, `card_eq_iff_eq_top`, `card_le_card_addGroup`, `card_le_of_le`, `card_le_one_iff_eq_bot`, `card_map_of_injective`, `card_subtype`, `card_top`, `closure_pi`, `eq_bot_iff_card`, `eq_bot_of_card_eq`, `eq_bot_of_card_le`, `eq_of_le_of_card_ge`, `eq_top_of_card_eq`, `eq_top_of_le_card`, `instFiniteSubtypeMem`, `list_sum_mem`, `multiset_noncommSum_mem`, `multiset_sum_mem`, `noncommSum_mem`, `one_lt_card_iff_ne_bot`, `pi_le_iff`, `pi_mem_of_single_mem`, `pi_mem_of_single_mem_aux`, `sum_mem`, `val_finset_sum`, `val_list_sum`, `val_multiset_sum`, `card_coeSort_mrange`, `card_coeSort_range`, `card_bot`, `card_eq_iff_eq_top`, `card_le_card_group`, `card_le_of_le`, `card_le_one_iff_eq_bot`, `card_map_of_injective`, `card_subtype`, `card_top`, `closure_pi`, `eq_bot_iff_card`, `eq_bot_of_card_eq`, `eq_bot_of_card_le`, `eq_of_le_of_card_ge`, `eq_top_of_card_eq`, `eq_top_of_le_card`, `instFiniteSubtypeMem`, `list_prod_mem`, `mem_normalizer_fintype`, `multiset_noncommProd_mem`, `multiset_prod_mem`, `noncommProd_mem`, `one_lt_card_iff_ne_bot`, `pi_le_iff`, `pi_mem_of_mulSingle_mem`, `pi_mem_of_mulSingle_mem_aux`, `prod_mem`, `val_finset_prod`, `val_list_prod`, `val_multiset_prod`	59
Total	69

AddMonoidHom

Definitions

Name	Category	Theorems
`decidableMemRange` 📖	CompOp	—
`fintypeMrange` 📖	CompOp	—
`fintypeRange` 📖	CompOp	—

AddSubgroup

Definitions

Name	Category	Theorems
`fintypeBot` 📖	CompOp	—
`instFintypeSubtypeMemOfDecidablePred` 📖	CompOp	3 math math: `image_range_addOrderOf`, `Fintype.card_zmultiples`, `card_zmultiples_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_bot` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot`	—	`mem_bot` `Nat.card_eq_fintype_card` `Fintype.card_unique`
`card_eq_iff_eq_top` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`eq_top_of_card_eq` `card_top`
`card_le_card_addGroup` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	—	`Nat.card_le_card_of_injective` `Subtype.coe_injective`
`card_le_of_le` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Nat.card` `SetLike.instMembership` `instSetLike`	—	`Nat.card_le_card_of_injective` `inclusion_injective`
`card_le_one_iff_eq_bot` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot`	—	`eq_bot_of_card_le` `mem_bot` `Nat.card_eq_fintype_card` `Fintype.card_unique` `le_refl`
`card_map_of_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike` `map`	—	`Nat.card_image_of_injective`
`card_subtype` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike` `map` `toAddGroup` `subtype`	—	`card_map_of_injective` `subtype_injective`
`card_top` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Nat.card_congr`
`closure_pi` 📖	mathematical	`Set` `Set.instMembership` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`closure` `Pi.addGroup` `Set.pi` `Set.univ` `pi`	—	`le_antisymm` `closure_le` `Set.pi_subset_pi_iff` `subset_closure` `pi_le_iff` `GaloisConnection.l_le` `gc_map_comap` `Set.mem_univ_pi` `Pi.single_eq_same` `Pi.single_eq_of_ne`
`eq_bot_iff_card` 📖	mathematical	—	`Bot.bot` `AddSubgroup` `instBot` `Nat.card` `SetLike.instMembership` `instSetLike`	—	`card_bot` `eq_bot_of_card_eq`
`eq_bot_of_card_eq` 📖	mathematical	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	`Bot.bot` `instBot`	—	`Nat.card_eq_one_iff_unique` `eq_bot_of_subsingleton`
`eq_bot_of_card_le` 📖	mathematical	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	`Bot.bot` `instBot`	—	`Finite.card_le_one_iff_subsingleton` `eq_bot_of_subsingleton`
`eq_of_le_of_card_ge` 📖	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Nat.card` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.coe_injective` `Set.Finite.eq_of_subset_of_card_le` `Set.toFinite`
`eq_top_of_card_eq` 📖	mathematical	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	`Top.top` `instTop`	—	`Nat.finite_of_card_ne_zero` `LT.lt.ne'` `Nat.card_pos` `Zero.instNonempty` `eq_top_of_le_card`
`eq_top_of_le_card` 📖	mathematical	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	`Top.top` `instTop`	—	`eq_of_le_of_card_ge` `instFiniteSubtypeMem` `le_top` `Nat.card_congr`
`instFiniteSubtypeMem` 📖	mathematical	—	`Finite` `AddSubgroup` `SetLike.instMembership` `instSetLike`	—	`Subtype.finite`
`list_sum_mem` 📖	mathematical	`AddSubgroup` `SetLike.instMembership` `instSetLike`	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`list_sum_mem` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`multiset_noncommSum_mem` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `Multiset.instMembership` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup` `SetLike.instMembership` `instSetLike`	`Multiset.noncommSum`	—	`AddSubmonoid.multiset_noncommSum_mem`
`multiset_sum_mem` 📖	mathematical	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike`	`Multiset.sum` `AddCommGroup.toAddCommMonoid`	—	`multiset_sum_mem` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`noncommSum_mem` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup` `SetLike.instMembership` `instSetLike`	`Finset.noncommSum`	—	`AddSubmonoid.noncommSum_mem`
`one_lt_card_iff_ne_bot` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	—	`lt_iff_not_ge` `Iff.not` `card_le_one_iff_eq_bot`
`pi_le_iff` 📖	mathematical	—	`AddSubgroup` `Pi.addGroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `pi` `Set.univ` `map` `AddMonoidHom.single` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`AddSubmonoid.pi_le_iff`
`pi_mem_of_single_mem` 📖	—	`AddSubgroup` `Pi.addGroup` `SetLike.instMembership` `instSetLike` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—	`AddSubmonoid.pi_mem_of_single_mem` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`pi_mem_of_single_mem_aux` 📖	—	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSubgroup` `Pi.addGroup` `SetLike.instMembership` `instSetLike` `Pi.single`	—	—	`AddSubmonoid.pi_mem_of_single_mem_aux` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`sum_mem` 📖	mathematical	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike`	`Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`sum_mem` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`val_finset_sum` 📖	mathematical	—	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `Finset.sum` `AddCommGroup.toAddCommMonoid` `toAddCommGroup`	—	`AddSubmonoidClass.coe_finset_sum` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`val_list_sum` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `instSetLike` `add` `zero` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddSubmonoidClass.coe_list_sum` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`
`val_multiset_sum` 📖	mathematical	—	`AddSubgroup` `AddCommGroup.toAddGroup` `SetLike.instMembership` `instSetLike` `Multiset.sum` `AddCommGroup.toAddCommMonoid` `toAddCommGroup` `Multiset.map`	—	`AddSubmonoidClass.coe_multiset_sum` `AddSubgroupClass.toAddSubmonoidClass` `instAddSubgroupClass`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_coeSort_mrange` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`card` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `MonoidHom.mrange` `MonoidHom.instMonoidHomClass` `MonoidHom.fintypeMrange`	—	`Set.card_range_of_injective`
`card_coeSort_range` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `MonoidHom.fintypeRange`	—	`Set.card_range_of_injective`

MonoidHom

Definitions

Name	Category	Theorems
`decidableMemRange` 📖	CompOp	2 math math: `AlternatingMap.domCoprod_coe`, `AlternatingMap.domCoprod_apply`
`fintypeMrange` 📖	CompOp	1 math math: `Fintype.card_coeSort_mrange`
`fintypeRange` 📖	CompOp	2 math math: `Fintype.card_coeSort_range`, `Equiv.Perm.OnCycleFactors.kerParam_range_card`

Subgroup

Definitions

Name	Category	Theorems
`fintypeBot` 📖	CompOp	—
`instFintypeSubtypeMemOfDecidablePred` 📖	CompOp	4 math math: `Equiv.Perm.OnCycleFactors.kerParam_range_card`, `image_range_orderOf`, `card_zpowers_le`, `Fintype.card_zpowers`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_bot` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot`	—	`Nat.card_eq_fintype_card` `Fintype.card_unique`
`card_eq_iff_eq_top` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`eq_top_of_card_eq` `card_top`
`card_le_card_group` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	—	`Nat.card_le_card_of_injective` `Subtype.coe_injective`
`card_le_of_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Nat.card` `SetLike.instMembership` `instSetLike`	—	`Nat.card_le_card_of_injective` `inclusion_injective`
`card_le_one_iff_eq_bot` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot`	—	`eq_bot_of_card_le` `Nat.card_eq_fintype_card` `Fintype.card_unique`
`card_map_of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `map`	—	`Nat.card_image_of_injective`
`card_subtype` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `map` `toGroup` `subtype`	—	`card_map_of_injective` `subtype_injective`
`card_top` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Nat.card_congr`
`closure_pi` 📖	mathematical	`Set` `Set.instMembership` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`closure` `Pi.group` `Set.pi` `Set.univ` `pi`	—	`le_antisymm` `closure_le` `Set.pi_subset_pi_iff` `subset_closure` `pi_le_iff` `GaloisConnection.l_le` `gc_map_comap` `Set.mem_univ_pi` `Pi.mulSingle_eq_same` `Pi.mulSingle_eq_of_ne`
`eq_bot_iff_card` 📖	mathematical	—	`Bot.bot` `Subgroup` `instBot` `Nat.card` `SetLike.instMembership` `instSetLike`	—	`card_bot` `eq_bot_of_card_eq`
`eq_bot_of_card_eq` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	`Bot.bot` `instBot`	—	`Nat.card_eq_one_iff_unique` `eq_bot_of_subsingleton`
`eq_bot_of_card_le` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	`Bot.bot` `instBot`	—	`Finite.card_le_one_iff_subsingleton` `eq_bot_of_subsingleton`
`eq_of_le_of_card_ge` 📖	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Nat.card` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.coe_injective` `Set.Finite.eq_of_subset_of_card_le` `Set.toFinite`
`eq_top_of_card_eq` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	`Top.top` `instTop`	—	`Nat.finite_of_card_ne_zero` `LT.lt.ne'` `Nat.card_pos` `One.instNonempty` `eq_top_of_le_card`
`eq_top_of_le_card` 📖	mathematical	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	`Top.top` `instTop`	—	`eq_of_le_of_card_ge` `instFiniteSubtypeMem` `le_top` `Nat.card_congr`
`instFiniteSubtypeMem` 📖	mathematical	—	`Finite` `Subgroup` `SetLike.instMembership` `instSetLike`	—	`Subtype.finite`
`list_prod_mem` 📖	mathematical	`Subgroup` `SetLike.instMembership` `instSetLike`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`list_prod_mem` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`mem_normalizer_fintype` 📖	mathematical	`Set` `Set.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`Subgroup` `SetLike.instMembership` `instSetLike` `setNormalizer`	—	`nonempty_fintype` `Set.eq_of_subset_of_card_le` `Set.card_image_of_injective` `conj_injective` `le_refl`
`multiset_noncommProd_mem` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `Multiset.instMembership` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup` `SetLike.instMembership` `instSetLike`	`Multiset.noncommProd`	—	`Submonoid.multiset_noncommProd_mem`
`multiset_prod_mem` 📖	mathematical	`Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `instSetLike`	`Multiset.prod` `CommGroup.toCommMonoid`	—	`multiset_prod_mem` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`noncommProd_mem` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup` `SetLike.instMembership` `instSetLike`	`Finset.noncommProd`	—	`Submonoid.noncommProd_mem`
`one_lt_card_iff_ne_bot` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	—	`lt_iff_not_ge` `Iff.not` `card_le_one_iff_eq_bot`
`pi_le_iff` 📖	mathematical	—	`Subgroup` `Pi.group` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `pi` `Set.univ` `map` `MonoidHom.mulSingle` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Submonoid.pi_le_iff`
`pi_mem_of_mulSingle_mem` 📖	—	`Subgroup` `Pi.group` `SetLike.instMembership` `instSetLike` `Pi.mulSingle` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—	`Submonoid.pi_mem_of_mulSingle_mem` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`pi_mem_of_mulSingle_mem_aux` 📖	—	`InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Subgroup` `Pi.group` `SetLike.instMembership` `instSetLike` `Pi.mulSingle`	—	—	`Submonoid.pi_mem_of_mulSingle_mem_aux` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`prod_mem` 📖	mathematical	`Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `instSetLike`	`Finset.prod` `CommGroup.toCommMonoid`	—	`prod_mem` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`val_finset_prod` 📖	mathematical	—	`Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `instSetLike` `Finset.prod` `CommGroup.toCommMonoid` `toCommGroup`	—	`SubmonoidClass.coe_finset_prod` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`val_list_prod` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `mul` `one` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`SubmonoidClass.coe_list_prod` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`
`val_multiset_prod` 📖	mathematical	—	`Subgroup` `CommGroup.toGroup` `SetLike.instMembership` `instSetLike` `Multiset.prod` `CommGroup.toCommMonoid` `toCommGroup` `Multiset.map`	—	`SubmonoidClass.coe_multiset_prod` `SubgroupClass.toSubmonoidClass` `instSubgroupClass`

---

← Back to Index