Finite

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

Statistics

Metric	Count
Definitions `subtypePermOfFintype`	1
Theorems `extendDomain`, `isConj_mul`, `orderOf`, `apply_mem_fixedPoints_iff_mem_of_mem_centralizer`, `disjoint_closure_of_disjoint_support`, `disjoint_ofSubtype_of_memFixedPoints_self`, `disjoint_of_disjoint_support`, `disjoint_support_closure_of_disjoint_support`, `isConj_of_support_equiv`, `mem_sumCongrHom_range_of_perm_mapsTo_inl`, `ofSubtype_support_disjoint`, `perm_inv_mapsTo_iff_mapsTo`, `perm_inv_mapsTo_of_mapsTo`, `perm_inv_on_of_perm_on_finite`, `perm_inv_on_of_perm_on_finset`, `perm_mapsTo_inl_iff_mapsTo_inr`, `perm_symm_mapsTo_iff_mapsTo`, `perm_symm_mapsTo_of_mapsTo`, `perm_symm_on_of_perm_on_finite`, `perm_symm_on_of_perm_on_finset`, `subtypePermOfFintype_apply`, `subtypePermOfFintype_one`, `support_closure_subset_union`, `support_pow_coprime`	24
Total	25

Equiv.Perm

Definitions

Name	Category	Theorems
`subtypePermOfFintype` 📖	CompOp	2 math math: `subtypePermOfFintype_apply`, `subtypePermOfFintype_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_fixedPoints_iff_mem_of_mem_centralizer` 📖	mathematical	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet`	`Set.instMembership` `Function.fixedPoints` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`mul_apply` `EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike`
`disjoint_closure_of_disjoint_support` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `support`	`Subgroup` `Equiv.Perm` `permGroup` `Subgroup.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `Subgroup.closure`	—	`disjoint_of_disjoint_support` `disjoint_support_closure_of_disjoint_support`
`disjoint_ofSubtype_of_memFixedPoints_self` 📖	mathematical	—	`Disjoint` `DFunLike.coe` `MonoidHom` `Equiv.Perm` `Set` `Set.instMembership` `Function.fixedPoints` `EquivLike.toFunLike` `Equiv.instEquivLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MonoidHom.instFunLike` `ofSubtype` `Function.fixedPoints.decidable`	—	`disjoint_iff_eq_or_eq` `ofSubtype_apply_of_not_mem`
`disjoint_of_disjoint_support` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `support`	`Subgroup` `Equiv.Perm` `permGroup` `Subgroup.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice`	—	`disjoint_iff_inf_le` `support_eq_empty_iff` `Finset.bot_eq_empty` `disjoint_self`
`disjoint_support_closure_of_disjoint_support` 📖	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `support` `Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.closure`	—	—	`support_closure_subset_union` `Set.disjoint_of_subset`
`isConj_of_support_equiv` 📖	mathematical	`Set` `Set.instMembership` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.Perm` `Finset.instMembership` `apply_mem_support`	`IsConj` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup`	—	`apply_mem_support` `isConj_iff` `Finite.of_fintype` `mul_inv_eq_iff_eq_mul` `ext` `Finset.mem_coe` `Equiv.extendSubtype_apply_of_mem` `mem_support` `Equiv.extendSubtype_not_mem`
`mem_sumCongrHom_range_of_perm_mapsTo_inl` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Set.range`	`Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `Prod.instGroup` `sumCongrHom`	—	`perm_mapsTo_inl_iff_mapsTo_inr` `Subtype.finite` `Finite.instSum` `Sum.inl_injective` `Sum.inr_injective` `MonoidHom.mem_range` `sumCongrHom_apply` `ext` `Equiv.sumCongr_apply` `Equiv.permCongr_apply` `Equiv.symm_symm` `Equiv.apply_ofInjective_symm` `Equiv.ofInjective_apply` `subtypePerm_apply`
`ofSubtype_support_disjoint` 📖	mathematical	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `support` `DFunLike.coe` `MonoidHom` `Equiv.Perm` `Set` `Set.instMembership` `Function.fixedPoints` `EquivLike.toFunLike` `Equiv.instEquivLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MonoidHom.instFunLike` `ofSubtype` `Function.fixedPoints.decidable`	—	`Finset.disjoint_iff_ne` `mem_support` `ofSubtype_apply_of_not_mem` `Function.mem_fixedPoints_iff`
`perm_inv_mapsTo_iff_mapsTo` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.Perm`	—	`perm_symm_mapsTo_iff_mapsTo`
`perm_inv_mapsTo_of_mapsTo` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv` `Equiv.symm`	—	`perm_symm_mapsTo_of_mapsTo`
`perm_inv_on_of_perm_on_finite` 📖	mathematical	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv` `Equiv.symm`	—	`perm_symm_on_of_perm_on_finite`
`perm_inv_on_of_perm_on_finset` 📖	mathematical	`Finset` `Finset.instMembership` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv` `Equiv.symm`	—	`perm_symm_on_of_perm_on_finset`
`perm_mapsTo_inl_iff_mapsTo_inr` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Set.range`	—	`perm_symm_mapsTo_iff_mapsTo` `Finite.Set.finite_range`
`perm_symm_mapsTo_iff_mapsTo` 📖	mathematical	—	`Set.MapsTo` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.Perm`	—	`perm_symm_mapsTo_of_mapsTo`
`perm_symm_mapsTo_of_mapsTo` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv` `Equiv.symm`	—	`nonempty_fintype` `Set.mem_toFinset` `perm_symm_on_of_perm_on_finset`
`perm_symm_on_of_perm_on_finite` 📖	mathematical	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv` `Equiv.symm`	—	`perm_symm_mapsTo_of_mapsTo`
`perm_symm_on_of_perm_on_finset` 📖	mathematical	`Finset` `Finset.instMembership` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv` `Equiv.symm`	—	`Finset.surj_on_of_inj_on_of_card_le` `Equiv.apply_eq_iff_eq` `Eq.ge` `Equiv.symm_apply_apply`
`subtypePermOfFintype_apply` 📖	mathematical	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`subtypePermOfFintype`	—	—
`subtypePermOfFintype_one` 📖	mathematical	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `instOne`	`subtypePermOfFintype`	—	—
`support_closure_subset_union` 📖	mathematical	`Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.closure`	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `Set.iUnion` `Set.instMembership`	—	`Subgroup.closure_induction` `Set.subset_iUnion₂_of_subset` `subset_rfl` `Set.instReflSubset` `support_one` `Finset.coe_empty` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Finset.coe_subset` `support_mul_le` `Finset.sup_eq_union` `Finset.coe_union` `Set.union_subset_iff` `support_inv`
`support_pow_coprime` 📖	mathematical	`orderOf` `Equiv.Perm` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup`	`support` `instPowNat`	—	`exists_pow_eq_self_of_coprime` `le_antisymm` `support_pow_le` `le_trans` `ge_of_eq`

Equiv.Perm.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extendDomain` 📖	mathematical	`Equiv.Perm.Disjoint`	`Equiv.Perm.extendDomain`	—	`Equiv.Perm.extendDomain_apply_subtype` `Equiv.apply_symm_apply` `Equiv.Perm.extendDomain_apply_not_subtype`
`isConj_mul` 📖	mathematical	`IsConj` `Equiv.Perm` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Equiv.Perm.Disjoint`	`Equiv.Perm.instMul`	—	`nonempty_fintype` `isConj_iff` `support_mul` `Finset.disjoint_coe` `Equiv.Perm.disjoint_iff_disjoint_support` `Equiv.Perm.isConj_of_support_equiv` `Finset.coe_union` `Equiv.Perm.support_conj` `Finset.coe_map` `Set.image_congr` `Equiv.Perm.apply_mem_support` `Set.mem_union` `Equiv.Perm.mul_apply` `Equiv.Perm.mem_support` `Finset.mem_coe` `Equiv.Set.union_apply_left` `Equiv.Perm.coe_inv` `Equiv.symm_apply_apply` `Equiv.apply_eq_iff_eq` `Equiv.Set.union_apply_right`
`orderOf` 📖	mathematical	`Equiv.Perm.Disjoint`	`orderOf` `Equiv.Perm` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Equiv.Perm.instMul`	—	`Commute.orderOf_mul_dvd_lcm` `commute` `orderOf_dvd_of_pow_eq_one` `Commute.mul_pow` `mul_eq_one_iff` `pow_disjoint_pow` `pow_orderOf_eq_one`

---

← Back to Index