Centralizer

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

Statistics

Metric	Count
Definitions `ofPermHom`, `ofPermHomFun`, `toCentralizer`, `toFun`, `cycleFactorsFinset_mulAction`, `instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset`, `kerParam`, `range_toPermHom'`, `toPermHom`, `instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset`	10
Theorems `card_ofPermHom_support`, `cycleOf_eq`, `injective`, `mem_fixedPoints_or_exists_zpow_eq`, `mem_support_self`, `mem_support_self'`, `nonempty`, `ofPermHomFun_apply_mem_support_cycle_iff`, `ofPermHomFun_apply_of_cycleOf_mem`, `ofPermHomFun_apply_of_mem_fixedPoints`, `ofPermHomFun_commute_zpow_apply`, `ofPermHomFun_mul`, `ofPermHomFun_one`, `ofPermHom_apply`, `ofPermHom_mem_centralizer`, `ofPermHom_support`, `sameCycle`, `toCentralizer_apply`, `toCentralizer_equivariant`, `toPermHom_apply_toCentralizer`, `toConjAct_smul_mem_cycleFactorsFinset`, `centralizer_smul_def`, `coe_toPermHom`, `cycleType_kerParam_apply_apply`, `kerParam_apply`, `kerParam_injective`, `kerParam_range_card`, `kerParam_range_eq`, `kerParam_range_le_centralizer`, `mem_ker_toPermHom_iff`, `mem_range_toPermHom'_iff`, `mem_range_toPermHom_iff`, `mem_range_toPermHom_iff'`, `nat_card_range_toPermHom`, `range_toPermHom_eq_range_toPermHom'`, `sign_kerParam_apply_apply`, `toPermHom_apply`, `val_centralizer_smul`, `card_isConj_eq`, `card_isConj_mul_eq`, `card_of_cycleType`, `card_of_cycleType_eq_zero_iff`, `card_of_cycleType_mul_eq`, `card_of_cycleType_singleton`, `nat_card_centralizer`	45
Total	55

Equiv.Perm

Definitions

Name	Category	Theorems
`instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset` 📖	CompOp	5 math math: `Basis.injective`, `Basis.sameCycle`, `Basis.mem_support_self`, `Basis.mem_fixedPoints_or_exists_zpow_eq`, `Basis.cycleOf_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_isConj_eq` 📖	mathematical	—	`Nat.card` `Set.Elem` `Equiv.Perm` `setOf` `IsConj` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Nat.factorial` `Fintype.card` `Multiset.sum` `Nat.instAddCommMonoid` `cycleType` `Multiset.prod` `Nat.instCommMonoid` `Finset.prod` `Multiset.toFinset` `Multiset.count`	—	`card_isConj_mul_eq` `nat_card_centralizer` `Nat.card_pos` `One.instNonempty` `Subgroup.instFiniteSubtypeMem` `Equiv.finite_left` `Finite.of_fintype`
`card_isConj_mul_eq` 📖	mathematical	—	`Nat.card` `Set.Elem` `Equiv.Perm` `setOf` `IsConj` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Nat.factorial` `Fintype.card` `Multiset.sum` `Nat.instAddCommMonoid` `cycleType` `Multiset.prod` `Nat.instCommMonoid` `Finset.prod` `Multiset.toFinset` `Multiset.count`	—	`Nat.card_eq_fintype_card` `nat_card_centralizer` `Subgroup.nat_card_centralizer_nat_card_stabilizer` `Fintype.card_congr'` `Set.ext` `ConjAct.card` `Fintype.card_perm` `MulAction.card_orbit_mul_card_stabilizer_eq_card_group`
`card_of_cycleType` 📖	mathematical	—	`Finset.card` `Equiv.Perm` `Finset.filter` `Multiset` `cycleType` `Multiset.decidableEq` `Finset.univ` `Equiv.instFintype` `Multiset.sum` `Nat.instAddCommMonoid` `Fintype.card` `Multiset.decidableDforallMultiset` `Nat.factorial` `Multiset.prod` `Nat.instCommMonoid` `Finset.prod` `Multiset.toFinset` `Multiset.count`	—	`symm` `IsEquiv.toSymm` `eq_isEquiv` `Multiset.prod_pos` `Nat.instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LT.lt.trans_le` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_two` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_pos` `Nat.factorial_pos` `Finset.prod_pos` `Nat.instNontrivial` `card_of_cycleType_mul_eq` `card_of_cycleType_eq_zero_iff`
`card_of_cycleType_eq_zero_iff` 📖	mathematical	—	`Finset.card` `Equiv.Perm` `Finset.filter` `Multiset` `cycleType` `Multiset.decidableEq` `Finset.univ` `Equiv.instFintype` `Multiset.sum` `Nat.instAddCommMonoid` `Fintype.card`	—	`Finset.card_eq_zero` `Finset.filter_eq_empty_iff` `exists_with_cycleType_iff`
`card_of_cycleType_mul_eq` 📖	mathematical	—	`Finset.card` `Equiv.Perm` `Finset.filter` `Multiset` `cycleType` `Multiset.decidableEq` `Finset.univ` `Equiv.instFintype` `Nat.factorial` `Fintype.card` `Multiset.sum` `Nat.instAddCommMonoid` `Multiset.prod` `Nat.instCommMonoid` `Finset.prod` `Multiset.toFinset` `Multiset.count` `Multiset.decidableDforallMultiset`	—	`exists_with_cycleType_iff` `Nat.card_eq_fintype_card` `Fintype.card_congr'` `isConj_comm` `card_isConj_mul_eq` `card_of_cycleType_eq_zero_iff` `MulZeroClass.zero_mul`
`card_of_cycleType_singleton` 📖	mathematical	`Fintype.card`	`Finset.card` `Equiv.Perm` `Finset.filter` `Multiset` `cycleType` `Multiset.instSingleton` `Multiset.decidableEq` `Finset.univ` `Equiv.instFintype` `Nat.factorial` `Nat.choose`	—	`mul_comm` `Nat.mul_factorial_pred` `mul_assoc` `Nat.factorial_ne_zero` `Nat.choose_mul_factorial_mul_factorial` `Multiset.sum_singleton` `Multiset.prod_singleton` `Finset.prod_congr` `Multiset.toFinset_singleton` `Finset.prod_singleton` `Multiset.count_eq_one_of_mem` `mul_one` `ite_and` `card_of_cycleType_mul_eq`
`nat_card_centralizer` 📖	mathematical	—	`Nat.card` `Equiv.Perm` `Subgroup` `permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Nat.factorial` `Fintype.card` `Multiset.sum` `Nat.instAddCommMonoid` `cycleType` `Multiset.prod` `Nat.instCommMonoid` `Finset.prod` `Multiset.toFinset` `Multiset.count`	—	`Subgroup.card_mul_index` `Subgroup.index_ker` `OnCycleFactors.nat_card_range_toPermHom` `OnCycleFactors.kerParam_range_card` `Nat.card_eq_fintype_card` `OnCycleFactors.kerParam_range_eq` `Subgroup.card_subtype`

Equiv.Perm.Basis

Definitions

Name	Category	Theorems
`ofPermHom` 📖	CompOp	4 math math: `card_ofPermHom_support`, `ofPermHom_apply`, `ofPermHom_mem_centralizer`, `ofPermHom_support`
`ofPermHomFun` 📖	CompOp	8 math math: `toCentralizer_apply`, `ofPermHom_apply`, `ofPermHomFun_commute_zpow_apply`, `ofPermHomFun_apply_mem_support_cycle_iff`, `ofPermHomFun_apply_of_mem_fixedPoints`, `ofPermHomFun_apply_of_cycleOf_mem`, `ofPermHomFun_mul`, `ofPermHomFun_one`
`toCentralizer` 📖	CompOp	3 math math: `toCentralizer_equivariant`, `toCentralizer_apply`, `toPermHom_apply_toCentralizer`
`toFun` 📖	CompOp	1 math math: `mem_support_self'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_ofPermHom_support` 📖	mathematical	—	`Finset.card` `Equiv.Perm.support` `DFunLike.coe` `MonoidHom` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `ofPermHom` `Finset.sum` `Nat.instAddCommMonoid` `Fintype.decidableEqEquivFintype` `Finset.Subtype.fintype`	—	`ofPermHom_support` `Finset.card_biUnion` `Equiv.Perm.Disjoint.disjoint_support` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `Subtype.prop` `Subtype.coe_ne_coe`
`cycleOf_eq` 📖	mathematical	—	`Equiv.Perm.cycleOf` `Equiv.Perm.instDecidableRelSameCycle` `DFunLike.coe` `Equiv.Perm.Basis` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset`	—	`Equiv.Perm.cycle_is_cycleOf` `mem_support_self` `Subtype.prop`
`injective` 📖	mathematical	—	`Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `DFunLike.coe` `Equiv.Perm.Basis` `Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset`	—	`Set.Pairwise.eq` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `Subtype.prop` `mem_support_self`
`mem_fixedPoints_or_exists_zpow_eq` 📖	mathematical	—	`Set` `Set.instMembership` `Function.fixedPoints` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Equiv.Perm.Basis` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset`	—	`Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff` `Equiv.Perm.mem_support` `Function.mem_fixedPoints_iff` `Equiv.Perm.mem_support_cycleOf_iff` `sameCycle`
`mem_support_self` 📖	mathematical	—	`Finset` `Finset.instMembership` `Equiv.Perm.support` `Equiv.Perm` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `DFunLike.coe` `Equiv.Perm.Basis` `Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset`	—	`mem_support_self'`
`mem_support_self'` 📖	mathematical	—	`Finset` `Finset.instMembership` `Equiv.Perm.support` `Equiv.Perm` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `toFun`	—	—
`nonempty` 📖	mathematical	—	`Equiv.Perm.Basis`	—	`Equiv.Perm.IsCycle.nonempty_support` `Equiv.Perm.mem_cycleFactorsFinset_iff` `Subtype.prop`
`ofPermHomFun_apply_mem_support_cycle_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `Equiv.Perm.support` `Equiv.Perm` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `ofPermHomFun`	—	`mem_fixedPoints_or_exists_zpow_eq` `ofPermHomFun_apply_of_mem_fixedPoints` `Equiv.Perm.notMem_support` `Function.mem_fixedPoints_iff` `Equiv.Perm.mem_cycleFactorsFinset_support_le` `Subtype.prop` `ofPermHomFun_apply_of_cycleOf_mem` `Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `Subtype.coe_ne_coe` `EquivLike.toEmbeddingLike` `Finset.disjoint_right` `Equiv.Perm.disjoint_iff_disjoint_support` `mem_support_self`
`ofPermHomFun_apply_of_cycleOf_mem` 📖	mathematical	`Finset` `Finset.instMembership` `Equiv.Perm.support` `Equiv.Perm` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Equiv.Perm.Basis` `Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset`	`ofPermHomFun` `Subgroup` `Subgroup.instSetLike` `Equiv.Perm.OnCycleFactors.range_toPermHom'`	—	`Equiv.Perm.cycle_is_cycleOf` `Subtype.prop` `Equiv.Perm.SameCycle.exists_nat_pow_eq` `Finite.of_fintype` `sameCycle` `Nat.find_spec` `zpow_natCast` `Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply` `Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset` `mem_support_self`
`ofPermHomFun_apply_of_mem_fixedPoints` 📖	mathematical	`Set` `Set.instMembership` `Function.fixedPoints` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`ofPermHomFun`	—	`ofPermHomFun.eq_1` `Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff` `Equiv.Perm.notMem_support`
`ofPermHomFun_commute_zpow_apply` 📖	mathematical	—	`ofPermHomFun` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Equiv.Perm.permGroup`	—	`mem_fixedPoints_or_exists_zpow_eq` `ofPermHomFun_apply_of_mem_fixedPoints` `Function.mem_fixedPoints_iff` `add_comm` `Equiv.Perm.mul_apply` `zpow_add_one` `zpow_add` `ofPermHomFun_apply_of_cycleOf_mem` `Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff`
`ofPermHomFun_mul` 📖	mathematical	—	`ofPermHomFun` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `Subgroup.mul`	—	`mem_fixedPoints_or_exists_zpow_eq` `ofPermHomFun_apply_of_mem_fixedPoints` `ofPermHomFun_apply_of_cycleOf_mem` `Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff` `mem_support_self`
`ofPermHomFun_one` 📖	mathematical	—	`ofPermHomFun` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `Subgroup.one`	—	`mem_fixedPoints_or_exists_zpow_eq` `ofPermHomFun_apply_of_mem_fixedPoints` `ofPermHomFun_apply_of_cycleOf_mem` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `OneMemClass.coe_one` `Equiv.Perm.coe_one`
`ofPermHom_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `ofPermHom` `ofPermHomFun`	—	—
`ofPermHom_mem_centralizer` 📖	mathematical	—	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `DFunLike.coe` `MonoidHom` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `ofPermHom`	—	`Subgroup.mem_centralizer_singleton_iff` `Equiv.Perm.ext` `ofPermHomFun_commute_zpow_apply`
`ofPermHom_support` 📖	mathematical	—	`Equiv.Perm.support` `DFunLike.coe` `MonoidHom` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `ofPermHom` `Finset.biUnion` `Fintype.decidableEqEquivFintype` `Finset.Subtype.fintype`	—	`Finset.ext` `mem_fixedPoints_or_exists_zpow_eq` `ofPermHomFun_apply_of_mem_fixedPoints` `Equiv.Perm.mem_support` `Equiv.Perm.mem_cycleFactorsFinset_support_le` `Subtype.prop` `Function.mem_fixedPoints_iff` `ofPermHomFun_apply_of_cycleOf_mem` `Equiv.injective` `injective` `not_iff_comm` `Mathlib.Tactic.Push.not_and_eq` `Equiv.Perm.notMem_support` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `Finset.disjoint_left` `Equiv.Perm.disjoint_iff_disjoint_support`
`sameCycle` 📖	mathematical	`Equiv.Perm` `Finset` `Finset.instMembership` `Equiv.Perm.cycleFactorsFinset` `Equiv.Perm.cycleOf` `Equiv.Perm.instDecidableRelSameCycle`	`Equiv.Perm.SameCycle` `DFunLike.coe` `Equiv.Perm.Basis` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset`	—	`Equiv.Perm.SameCycle.symm` `Equiv.Perm.mem_support_cycleOf_iff` `mem_support_self`
`toCentralizer_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `MonoidHom` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `toCentralizer` `ofPermHomFun`	—	—
`toCentralizer_equivariant` 📖	mathematical	—	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Equiv.Perm.OnCycleFactors.instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset` `DFunLike.coe` `MonoidHom` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `toCentralizer` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.Perm.ext` `Equiv.Perm.mem_cycleFactorsFinset_iff` `Subtype.prop` `ofPermHomFun_commute_zpow_apply` `zpow_one` `ofPermHomFun_apply_mem_support_cycle_iff` `Equiv.Perm.notMem_support`
`toPermHom_apply_toCentralizer` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `Equiv.Perm.OnCycleFactors.toPermHom` `Equiv.Perm.OnCycleFactors.range_toPermHom'` `toCentralizer`	—	`Equiv.Perm.ext` `Equiv.Perm.OnCycleFactors.toPermHom_apply` `toCentralizer_equivariant`

Equiv.Perm.OnCycleFactors

Definitions

Name	Category	Theorems
`instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset` 📖	CompOp	4 math math: `Equiv.Perm.Basis.toCentralizer_equivariant`, `val_centralizer_smul`, `toPermHom_apply`, `centralizer_smul_def`
`kerParam` 📖	CompOp	8 math math: `kerParam_range_card`, `kerParam_injective`, `cycleType_kerParam_apply_apply`, `kerParam_range_eq_centralizer_of_count_le_one`, `kerParam_range_le_centralizer`, `kerParam_range_eq`, `kerParam_apply`, `sign_kerParam_apply_apply`
`range_toPermHom'` 📖	CompOp	13 math math: `Equiv.Perm.Basis.toCentralizer_equivariant`, `Equiv.Perm.Basis.toCentralizer_apply`, `Equiv.Perm.Basis.card_ofPermHom_support`, `Equiv.Perm.Basis.ofPermHom_apply`, `mem_range_toPermHom'_iff`, `Equiv.Perm.Basis.ofPermHom_mem_centralizer`, `Equiv.Perm.Basis.toPermHom_apply_toCentralizer`, `Equiv.Perm.Basis.ofPermHom_support`, `Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff`, `Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem`, `Equiv.Perm.Basis.ofPermHomFun_mul`, `Equiv.Perm.Basis.ofPermHomFun_one`, `range_toPermHom_eq_range_toPermHom'`
`toPermHom` 📖	CompOp	9 math math: `mem_range_toPermHom_iff'`, `nat_card_range_toPermHom`, `Equiv.Perm.Basis.toPermHom_apply_toCentralizer`, `mem_ker_toPermHom_iff`, `coe_toPermHom`, `mem_range_toPermHom_iff`, `toPermHom_apply`, `kerParam_range_eq`, `range_toPermHom_eq_range_toPermHom'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centralizer_smul_def` 📖	mathematical	—	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset` `Equiv.Perm.instMul` `Subgroup.inv` `Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset` `Subtype.prop`	—	—
`coe_toPermHom` 📖	mathematical	—	`Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `toPermHom` `Equiv.Perm.instMul` `Equiv.Perm.instInv`	—	—
`cycleType_kerParam_apply_apply` 📖	mathematical	—	`Equiv.Perm.cycleType` `DFunLike.coe` `MonoidHom` `Equiv.Perm` `Set.Elem` `Function.fixedPoints` `EquivLike.toFunLike` `Equiv.instEquivLike` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Pi.mulOneClass` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `MonoidHom.instFunLike` `kerParam` `Multiset` `Multiset.instAdd` `Subtype.fintype` `Set` `Set.instMembership` `Function.fixedPoints.decidable` `Finset.sum` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `Finset.univ` `Finset.Subtype.fintype`	—	`Subtype.prop` `Equiv.Perm.Disjoint.zpow_disjoint_zpow` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `Subtype.coe_ne_coe` `Equiv.Perm.pairwise_commute_of_mem_zpowers` `Equiv.Perm.commute_ofSubtype_noncommPiCoprod` `kerParam.eq_1` `MonoidHom.noncommCoprod_apply` `Prod.fst_mul_snd` `mul_one` `one_mul` `Finset.univ_eq_attach` `Equiv.Perm.Disjoint.cycleType_mul` `Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod` `Subgroup.noncommPiCoprod_apply` `Set.Pairwise.imp` `Equiv.Perm.Disjoint.commute` `Equiv.Perm.Disjoint.cycleType_noncommProd` `Equiv.Perm.cycleType_ofSubtype`
`kerParam_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `Set.Elem` `Function.fixedPoints` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Pi.mulOneClass` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `MonoidHom.instFunLike` `kerParam` `Finset.instMembership` `Equiv.Perm.cycleOf` `Equiv.Perm.instDecidableRelSameCycle` `Finset.decidableMem` `Fintype.decidableEqEquivFintype` `Set` `Set.instMembership` `Equiv.Perm.ofSubtype` `Function.fixedPoints.decidable`	—	`Equiv.Perm.pairwise_commute_of_mem_zpowers` `Equiv.Perm.commute_ofSubtype_noncommPiCoprod` `kerParam.eq_1` `MonoidHom.noncommCoprod_apply'` `Equiv.Perm.mul_apply` `Equiv.Perm.ofSubtype_apply_of_not_mem` `Function.mem_fixedPoints_iff` `Equiv.Perm.mem_support` `Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff` `Subtype.prop` `Subgroup.noncommPiCoprod_apply` `Finset.noncommProd_erase_mul` `Finset.mem_univ` `Finset.mem_of_mem_erase` `Equiv.Perm.notMem_support` `Mathlib.Tactic.Contrapose.contrapose₄` `Equiv.Perm.mem_support_of_mem_noncommProd_support` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `Subgroup.mem_zpowers_iff` `Finset.disjoint_left` `Equiv.Perm.disjoint_iff_disjoint_support` `Equiv.Perm.support_zpow_le` `Equiv.Perm.cycleOf_apply_self` `Equiv.Perm.zpow_apply_mem_support` `MonoidHom.noncommCoprod_apply` `Equiv.apply_eq_iff_eq` `Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le`
`kerParam_injective` 📖	mathematical	—	`Equiv.Perm` `Set.Elem` `Function.fixedPoints` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Pi.mulOneClass` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `MonoidHom.instFunLike` `kerParam`	—	`Equiv.Perm.pairwise_commute_of_mem_zpowers` `Equiv.Perm.commute_ofSubtype_noncommPiCoprod` `kerParam.eq_1` `MonoidHom.noncommCoprod_injective` `Equiv.Perm.ofSubtype_injective` `MonoidHom.injective_noncommPiCoprod_of_iSupIndep` `Subgroup.commute_subtype_of_commute` `Subgroup.range_subtype` `iSup_congr_Prop` `Subgroup.zpowers_eq_closure` `Equiv.Perm.disjoint_closure_of_disjoint_support` `Equiv.Perm.disjoint_iff_disjoint_support` `Equiv.Perm.cycleFactorsFinset_pairwise_disjoint` `Subgroup.subtype_injective` `Subgroup.noncommPiCoprod_range` `Subgroup.closure_eq` `Disjoint.mono_right` `Equiv.Perm.mem_cycleFactorsFinset_support_le` `Equiv.Perm.ofSubtype_support_disjoint`
`kerParam_range_card` 📖	mathematical	—	`Fintype.card` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.range` `Set.Elem` `Function.fixedPoints` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Prod.instGroup` `Pi.group` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup.zpowers` `Subgroup.toGroup` `kerParam` `MonoidHom.fintypeRange` `instFintypeProd` `Equiv.instFintype` `Set` `Set.instMembership` `Subtype.fintype` `Function.fixedPoints.decidable` `Pi.instFintype` `Fintype.decidableEqEquivFintype` `Finset.Subtype.fintype` `Subgroup.instFintypeSubtypeMemOfDecidablePred` `Subgroup.decidableMemZPowers` `Nat.factorial` `Multiset.sum` `Nat.instAddCommMonoid` `Equiv.Perm.cycleType` `Multiset.prod` `Nat.instCommMonoid`	—	`Fintype.card_coeSort_range` `kerParam_injective` `Fintype.card_prod` `Fintype.card_perm` `Fintype.card_pi` `Equiv.Perm.card_fixedPoints` `Finset.univ_eq_attach` `Finset.prod_attach` `Equiv.Perm.cycleType.eq_1` `Finset.prod_map_val` `Finset.prod_congr` `Fintype.card_zpowers` `Equiv.Perm.IsCycle.orderOf` `Equiv.Perm.mem_cycleFactorsFinset_iff`
`kerParam_range_eq` 📖	mathematical	—	`MonoidHom.range` `Equiv.Perm` `Set.Elem` `Function.fixedPoints` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Prod.instGroup` `Equiv.Perm.permGroup` `Pi.group` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `kerParam` `Subgroup.map` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Subgroup.subtype` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toPermHom`	—	`le_antisymm` `Equiv.Perm.pairwise_commute_of_mem_zpowers` `Equiv.Perm.commute_ofSubtype_noncommPiCoprod` `kerParam.eq_1` `MonoidHom.noncommCoprod_range` `sup_le_iff` `Subgroup.noncommPiCoprod_range` `iSup_le_iff` `Subgroup.mem_centralizer_singleton_iff` `Equiv.Perm.Disjoint.commute` `Equiv.Perm.disjoint_iff_disjoint_support` `Equiv.Perm.ofSubtype_support_disjoint` `Equiv.Perm.ext` `Commute.mul_inv_cancel` `Disjoint.mono_right` `Equiv.Perm.mem_cycleFactorsFinset_support_le` `Equiv.Perm.self_mem_cycle_factors_commute` `Equiv.Perm.cycleFactorsFinset_mem_commute'` `Equiv.Perm.apply_mem_fixedPoints_iff_mem_of_mem_centralizer` `Subtype.prop` `kerParam_apply` `Equiv.Perm.mem_support` `Equiv.Perm.cycleOf_apply_self` `Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff` `Equiv.Perm.ofSubtype_apply_of_mem` `Equiv.Perm.subtypePerm_apply` `Equiv.Perm.notMem_support`
`kerParam_range_le_centralizer` 📖	mathematical	—	`Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.range` `Set.Elem` `Function.fixedPoints` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Prod.instGroup` `Pi.group` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `kerParam` `Subgroup.centralizer` `Set` `Set.instSingletonSet`	—	`kerParam_range_eq` `Subgroup.map_subtype_le`
`mem_ker_toPermHom_iff` 📖	mathematical	—	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Subgroup.toGroup` `MonoidHom.ker` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toPermHom` `Commute` `Equiv.Perm.instMul`	—	—
`mem_range_toPermHom'_iff` 📖	mathematical	—	`Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `range_toPermHom'` `Finset.card` `Equiv.Perm.support` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`mem_range_toPermHom_iff` 📖	mathematical	—	`Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `MonoidHom.range` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Subgroup.toGroup` `toPermHom` `Finset.card` `Equiv.Perm.support` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`coe_toPermHom` `Equiv.Perm.support_conj` `Finset.card_map` `Equiv.Perm.Basis.nonempty` `Equiv.Perm.Basis.toPermHom_apply_toCentralizer`
`mem_range_toPermHom_iff'` 📖	mathematical	—	`Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `MonoidHom.range` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Subgroup.toGroup` `toPermHom` `Finset.card` `Equiv.Perm.support` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`mem_range_toPermHom_iff`
`nat_card_range_toPermHom` 📖	mathematical	—	`Nat.card` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `MonoidHom.range` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Subgroup.toGroup` `toPermHom` `Finset.prod` `Nat.instCommMonoid` `Multiset.toFinset` `Equiv.Perm.cycleType` `Nat.factorial` `Multiset.count`	—	`Fintype.card_eq_nat_card` `mem_range_toPermHom_iff'` `Set.mem_setOf_eq` `Nat.card_eq_fintype_card` `Fintype.card_congr'` `DomMulAct.stabilizer_card'` `Finset.prod_congr` `Finset.ext` `Multiset.map_congr`
`range_toPermHom_eq_range_toPermHom'` 📖	mathematical	—	`MonoidHom.range` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Subgroup.toGroup` `Finset` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `toPermHom` `range_toPermHom'`	—	`Subgroup.ext` `mem_range_toPermHom_iff` `mem_range_toPermHom'_iff`
`sign_kerParam_apply_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `Units` `Int.instMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `Equiv.Perm.sign` `Set.Elem` `Function.fixedPoints` `EquivLike.toFunLike` `Equiv.instEquivLike` `Prod.instMulOneClass` `Pi.mulOneClass` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `kerParam` `Units.instMul` `Set` `Set.instMembership` `Subtype.fintype` `Function.fixedPoints.decidable` `Finset.prod` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `Int.instCommMonoid` `Finset.univ` `Finset.Subtype.fintype`	—	`Equiv.Perm.pairwise_commute_of_mem_zpowers` `Equiv.Perm.commute_ofSubtype_noncommPiCoprod` `kerParam.eq_1` `MonoidHom.noncommCoprod_apply` `Prod.fst_mul_snd` `mul_one` `one_mul` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Equiv.Perm.sign_ofSubtype` `Finset.univ_eq_attach` `LeftCancelSemigroup.toIsLeftCancelMul` `MonoidHom.comp_apply` `Subgroup.commute_subtype_of_commute` `Subgroup.noncommPiCoprod.eq_1` `Pairwise.mono` `MonoidHom.comp_noncommPiCoprod` `Pairwise.set_pairwise` `MonoidHom.noncommPiCoprod_apply` `Commute.all` `Finset.noncommProd_eq_prod` `Finset.prod_congr`
`toPermHom_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MonoidHom.instFunLike` `toPermHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset`	—	—
`val_centralizer_smul` 📖	mathematical	—	`Equiv.Perm` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Equiv.Perm.permGroup` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `instMulActionSubtypeMemSubgroupCentralizerSingletonSetFinsetCycleFactorsFinset` `Equiv.Perm.instMul` `Subgroup.inv`	—	—

Equiv.Perm.OnCycleFactors.Subgroup.Centralizer

Definitions

Name	Category	Theorems
`cycleFactorsFinset_mulAction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toConjAct_smul_mem_cycleFactorsFinset` 📖	mathematical	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `Finset` `Finset.instMembership` `Equiv.Perm.cycleFactorsFinset`	`ConjAct` `ConjAct.instSMul` `Group.toDivInvMonoid` `DFunLike.coe` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `ConjAct.instDivInvMonoid` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `ConjAct.toConjAct`	—	`Equiv.Perm.cycleFactorsFinset_conj_eq` `mul_inv_cancel` `mul_one` `mul_assoc` `Subgroup.mem_centralizer_singleton_iff` `ConjAct.toConjAct_smul` `Finset.coe_smul_finset` `Finset.mem_coe`

---

← Back to Index