| Metric | Count |
|---|
Definitionsconj, instGroup, instInhabited, toPerm, AddAutAdditive, equivUnitsEnd, extendDomainHom, instInv, instMul, instOne, instPowNat, ofSubtype, permCongrHom, permGroup, sigmaCongrRightHom, subtypeCongrHom, subtypeEquivSubtypePerm, subtypePerm, sumCongrHom, permCongrHom, toHomPerm, MulAut, conj, instGroup, instInhabited, toPerm, MulAutMultiplicative, instInhabitedEnd, instMonoidEnd | 29 |
Theoremsapply_inv_self, coe_inv, coe_mul, coe_one, congr_apply, congr_symm_apply, conj_apply, conj_inv_apply, conj_symm_apply, inv_apply, inv_apply_self, inv_def, inv_symm, mul_apply, mul_def, neg_conj_apply, one_apply, one_def, symm_inv, AddAutAdditive_apply_apply, AddAutAdditive_apply_symm_apply, AddAutAdditive_symm_apply_apply, AddAutAdditive_symm_apply_symm_apply, apply_inv_self, coe_inv, coe_mul, coe_one, coe_pow, default_eq, eq_inv_iff_eq, equivUnitsEnd_symm_apply_apply, equivUnitsEnd_symm_apply_symm_apply, extendDomainHom_apply, extendDomainHom_injective, extendDomain_eq_one_iff, extendDomain_inv, extendDomain_mul, extendDomain_one, extendDomain_pow, extendDomain_zpow, inv_apply_self, inv_def, inv_eq_iff_eq, inv_subtypePerm, inv_trans_self, iterate_eq_pow, mul_apply, mul_def, mul_refl, mul_symm, ofSubtype_apply_coe, ofSubtype_apply_mem_iff_mem, ofSubtype_apply_of_mem, ofSubtype_apply_of_not_mem, ofSubtype_injective, ofSubtype_subtypePerm, ofSubtype_subtypePerm_of_mem, ofSubtype_subtypePerm_of_not_mem, one_apply, one_def, one_symm, one_trans, permCongr_eq_mul, refl_inv, refl_mul, self_trans_inv, sigmaCongrRightHom_apply, sigmaCongrRightHom_injective, sigmaCongrRight_inv, sigmaCongrRight_mul, sigmaCongrRight_one, subtypeCongrHom_apply, subtypeCongrHom_injective, subtypeEquivSubtypePerm_apply_coe, subtypeEquivSubtypePerm_apply_of_mem, subtypeEquivSubtypePerm_apply_of_not_mem, subtypeEquivSubtypePerm_symm_apply, subtypePerm_apply, subtypePerm_inv, subtypePerm_mul, subtypePerm_ofSubtype, subtypePerm_one, subtypePerm_pow, subtypePerm_zpow, sumCongrHom_apply, sumCongrHom_injective, sumCongr_inv, sumCongr_mul, sumCongr_one, sumCongr_one_swap, sumCongr_swap_one, symm_mul, trans_one, val_equivUnitsEnd_apply, val_inv_equivUnitsEnd_apply, zpow_apply_comm, addLeft_add, addLeft_zero, addRight_add, addRight_zero, inv_mulLeft, inv_mulRight, mulLeft_mul, mulLeft_one, mulRight_mul, mulRight_one, mul_swap_eq_iff, mul_swap_eq_swap_mul, mul_swap_involutive, mul_swap_mul_self, neg_addLeft, neg_addRight, nsmul_addLeft, nsmul_addRight, permCongrHom_coe, permCongrHom_coe_equiv, permCongrHom_symm, permCongrHom_trans, permCongr_eq_mul, permCongr_mul, pow_mulLeft, pow_mulRight, swap_apply_apply, swap_eq_one_iff, swap_inv, swap_mul_eq_iff, swap_mul_eq_mul_swap, swap_mul_involutive, swap_mul_self, swap_mul_self_mul, swap_mul_swap_mul_swap, zpow_mulLeft, zpow_mulRight, zsmul_addLeft, zsmul_addRight, toHomPerm_apply_apply, toHomPerm_apply_symm_apply, apply_inv_self, coe_inv, coe_mul, coe_one, congr_apply, congr_symm_apply, conj_apply, conj_inv_apply, conj_symm_apply, inv_apply, inv_apply_self, inv_def, inv_symm, mul_apply, mul_def, one_apply, one_def, symm_inv, MulAutMultiplicative_apply_apply, MulAutMultiplicative_apply_symm_apply, MulAutMultiplicative_symm_apply_apply, MulAutMultiplicative_symm_apply_symm_apply | 159 |
| Total | 188 |
| Name | Category | Theorems |
|---|
equivUnitsEnd 📖 | CompOp | 4 mathmath: val_equivUnitsEnd_apply, equivUnitsEnd_symm_apply_symm_apply, equivUnitsEnd_symm_apply_apply, val_inv_equivUnitsEnd_apply
|
extendDomainHom 📖 | CompOp | 2 mathmath: extendDomainHom_apply, extendDomainHom_injective
|
instInv 📖 | CompOp | 67 mathmath: sameCycle_conj, cycleOf_inv, mem_cycleFactorsFinset_conj, Matrix.transpose_permMatrix, apply_inv_self, Equiv.swap_apply_apply, cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, disjoint_inv_right_iff, cycleFactorsFinset_mul_inv_mem_eq_sdiff, permCongr_eq_mul, Tuple.sort_perm, Matrix.permMatrixHom_apply, IsCycle.conj, sumCongr_inv, Function.IsFixedPt.perm_inv, Matrix.conjTranspose_permMatrix, Equiv.neg_addLeft, Rack.ad_conj, inv_eq_iff_eq, extendDomain_inv, image_inv, isCycle_inv, Disjoint.inv_right, signAux_inv, sameCycle_inv, preimage_inv, IsCycleOn.inv, Rack.invAct_apply, inv_apply_self, Equiv.neg_addRight, IsThreeCycle.inv_iff, Equiv.inv_mulRight, isCycleOn_inv, refl_inv, disjoint_conj, sigmaCongrRight_inv, coe_inv, SameCycle.inv, Equiv.swap_mul_eq_mul_swap, IsThreeCycle.inv, Equiv.swap_inv, support_inv, disjoint_inv_left_iff, inv_subtypePerm, OnCycleFactors.coe_toPermHom, Set.BijOn.perm_inv, Disjoint.inv_left, SameCycle.conj, inv_def, cycleType_conj, support_conj, IsCycle.inv, card_support_conj, Equiv.permCongr_eq_mul, Disjoint.conj, Cycle.formPerm_reverse, cycleType_inv, sign_inv, RootPairing.reflectionPerm_inv, self_trans_inv, List.formPerm_reverse, eq_inv_iff_eq, disjoint_mul_inv_of_mem_cycleFactorsFinset, IsCycleOn.conj, Equiv.inv_mulLeft, RootPairing.Equiv.indexEquiv_inv, inv_trans_self
|
instMul 📖 | CompOp | 123 mathmath: sameCycle_conj, subtypePerm_mul, mem_cycleFactorsFinset_conj, support_prod_of_pairwise_disjoint, card_support_swap_mul, map_equiv_removeNone, Equiv.swap_apply_apply, Equiv.addRight_add, val_equivUnitsEnd_apply, cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, Equiv.swap_mul_self, eq_on_support_mem_disjoint, symm_mul, cycleFactorsFinset_mul_inv_mem_eq_sdiff, set_support_mul_subset, permCongr_eq_mul, Disjoint.cycleType, Disjoint.commute, IsCycle.commute_iff', coe_mul, IsCycle.conj, alternatingGroup.normalClosure_swap_mul_swap_five, support_swap_mul_eq, support_swap_mul_swap, mul_mem_alternatingGroup_of_isSwap, cycleType_swap_mul_swap_of_nodup, Disjoint.card_support_mul, commute_iff_of_mem_cycleFactorsFinset, Equiv.permCongrHom_coe, mem_list_cycles_iff, Rack.ad_conj, Matrix.permMatrix_mul, isCycle_swap_mul_aux₁, self_mem_cycle_factors_commute, Equiv.addLeft_add, Disjoint.support_mul, extendDomain_mul, Equiv.swap_mul_involutive, support_noncommProd, disjoint_prod_right, Disjoint.mul_apply_eq_iff, isThreeCycle_sq_of_three_mem_cycleType_five, Equiv.mul_swap_eq_swap_mul, mem_cycleType_iff, Equiv.swap_mul_eq_iff, OnCycleFactors.val_centralizer_smul, support_mul_le, card_support_prod_list_of_pairwise_disjoint, Equiv.mul_swap_involutive, mul_def, disjoint_conj, sign_mul, Equiv.swap_mul_eq_mul_swap, OnCycleFactors.mem_ker_toPermHom_iff, IsThreeCycle.eq_swap_mul_swap_iff_mem_support, mul_symm, refl_mul, signAux3_mul_and_swap, Equiv.permCongr_mul, List.zipWith_swap_prod_support', isCycle_swap_mul_aux₂, support_swap_mul_ge_support_diff, Equiv.permCongrHom_symm, Equiv.mul_swap_mul_self, sumCongr_mul, Equiv.mul_swap_eq_iff, OnCycleFactors.coe_toPermHom, Equiv.swap_mul_swap_mul_swap, SameCycle.conj, swap_mul_swap_same_mem_closure_three_cycles, support_prod_le, cycleType_conj, prod_list_swap_mem_alternatingGroup_iff_even_length, support_conj, IsSwap.mul_mem_closure_three_cycles, DomMulAct.stabilizerMulEquiv_apply, Disjoint.mul_eq_one_iff, Disjoint.mul_right, card_support_conj, IsThreeCycle.isThreeCycle_sq, Equiv.swap_mul_self_mul, Equiv.permCongr_eq_mul, IsCycle.swap_mul, disjoint_prod_perm, Disjoint.conj, cycleFactorsFinset_mem_commute, Disjoint.mul_left, equivUnitsEnd_symm_apply_symm_apply, Equiv.permCongrHom_coe_equiv, cycleFactorsFinset_eq_list_toFinset, MultilinearMap.domDomCongr_mul, List.formPerm_cons_cons, mul_apply, equivUnitsEnd_symm_apply_apply, Disjoint.cycleType_mul, IsCycle.forall_commute_iff, alternatingGroup.isConj_swap_mul_swap_of_cycleType_two, Equiv.mulRight_mul, mul_refl, decomposeOption_symm_apply, Disjoint.orderOf, IsCycle.commute_iff, prod_prodExtendRight, Disjoint.cycleFactorsFinset_mul_eq_union, Disjoint.isConj_mul, sign_prod_list_swap, cycleFactorsFinset_mem_commute', List.zipWith_swap_prod_support, disjoint_mul_inv_of_mem_cycleFactorsFinset, Equiv.mulLeft_mul, support_le_prod_of_mem, IsCycleOn.conj, val_inv_equivUnitsEnd_apply, isThreeCycle_swap_mul_swap_same, Equiv.constVAdd_add, Equiv.permCongrHom_trans, List.formPerm_append_pair, sigmaCongrRight_mul, Disjoint.cycleOf_mul_distrib, OnCycleFactors.centralizer_smul_def, signAux_mul, commute_ofSubtype_noncommPiCoprod, LinearMap.IsSymmetric.eigenvectorBasis_def
|
instOne 📖 | CompOp | 87 mathmath: Fin.cycleIcc_ge, support_prod_of_pairwise_disjoint, Cycle.formPerm_subsingleton, disjoint_refl_iff, cycleFactorsFinset_eq_empty_iff, card_support_le_one, Equiv.constVAdd_zero, support_eq_empty_iff, RootPairing.reflectionPerm_sq, Equiv.swap_mul_self, eq_on_support_mem_disjoint, symm_mul, IsCycle.pow_eq_one_iff', disjoint_one_left, cycleOf_eq_one_iff, support_one, one_def, List.formPerm_singleton, card_support_eq_zero, cycleOf_one, Equiv.optionCongr_one, Equiv.swap_eq_one_iff, mem_list_cycles_iff, Fin.cycleRange_zero, AddAction.toPerm_zero, default_eq, signAux_one, IsCycle.pow_eq_one_iff, cycleFactorsFinset_one, disjoint_prod_right, Equiv.mulLeft_one, sigmaCongrRight_one, coe_one, trans_one, Equiv.addRight_zero, Matrix.permMatrix_one, refl_inv, card_support_prod_list_of_pairwise_disjoint, one_trans, IsCycle.cycleOf, sumCongr_swap_one, one_symm, mul_symm, List.zipWith_swap_prod_support', sumCongr_one_swap, Fin.cycleIcc_def_gt, sumCongr_one, cycleType_eq_zero, card_cycleType_eq_zero, Set.powersetCard.addAction_faithful, List.formPerm_pow_length_eq_one_of_nodup, toList_one, support_prod_le, prod_list_swap_mem_alternatingGroup_iff_even_length, cycleType_one, decomposeFin_symm_of_one, Fin.cycleRange_mk_zero, disjoint_one_right, Disjoint.mul_eq_one_iff, IsCycle.pow_eq_one_iff'', extendDomain_one, one_apply, Fin.cycleIcc_eq, disjoint_prod_perm, Set.Subsingleton.isCycleOn_one, List.formPerm_eq_one_iff, cycleFactorsFinset_eq_list_toFinset, Set.powersetCard.mulAction_faithful, Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia, isCycleOn_one, self_trans_inv, sign_one, extendDomain_eq_one_iff, prod_prodExtendRight, sameCycle_one, pow_prime_eq_one_iff, Equiv.addLeft_zero, sign_prod_list_swap, not_isCycle_one, List.zipWith_swap_prod_support, monotone_iff, support_le_prod_of_mem, Equiv.mulRight_one, Fin.cycleIcc_def_gt', MulAction.toPerm_one, List.formPerm_nil, inv_trans_self
|
instPowNat 📖 | CompOp | 65 mathmath: SameCycle.exists_pow_eq_of_mem_support, SameCycle.exists_pow_eq, Finset.product_self_eq_disjiUnion_perm_aux, SameCycle.exists_nat_pow_eq, IsCycle.exists_pow_eq, iterate_eq_pow, IsCycleOn.exists_pow_eq', IsCycle.pow_eq_one_iff', IsCycle.pow_iff, support_pow_le, pow_eq_on_of_mem_support, cycleOf_apply_apply_pow_self, SameCycle.exists_pow_eq', cycleOf_pow_apply_self, SameCycle.exists_fin_pow_eq, Equiv.nsmul_addLeft, SameCycle.pow_right, IsCycleOn.exists_pow_eq, Equiv.pow_mulLeft, IsCycle.pow_eq_one_iff, extendDomain_pow, closure_cycle_coprime_swap, cycleOf_self_apply_pow, Function.IsFixedPt.perm_pow, Disjoint.pow_disjoint_pow, IsCycle.support_pow_eq_iff, IsCycleOn.pow_card_apply, Equiv.nsmul_addRight, IsCycle.pow_eq_pow_iff, List.formPerm_pow_apply_head, IsCycleOn.range_pow, apply_pow_apply_eq_iff, Set.BijOn.perm_pow, getElem_toList, List.formPerm_pow_apply_getElem, toList_pow_apply_eq_rotate, Set.MapsTo.perm_pow, sameCycle_pow_right, subtypePerm_apply_pow_of_mem, IsCycle.zpowersEquivSupport_apply, IsCycle.support_pow_of_pos_of_lt_orderOf, pow_apply_eq_self_of_apply_eq_self, pow_apply_mem_support, pow_apply_eq_of_apply_apply_eq_self, IsCycleOn.pow_apply_eq_pow_apply, List.formPerm_pow_length_eq_one_of_nodup, pow_mod_card_support_cycleOf_self_apply, pow_apply_mem_toList_iff_mem_support, Finset.sum_smul_sum_eq_sum_perm, Finset.sum_mul_sum_eq_sum_perm, IsCycle.pow_eq_one_iff'', support_pow_coprime, IsCycle.zpowersEquivSupport_symm_apply, IsCycle.isCycle_pow_pos_of_lt_prime_order, Set.SurjOn.perm_pow, sameCycle_pow_left, pow_prime_eq_one_iff, pow_mod_orderOf_cycleOf_apply, SameCycle.pow_left, subtypePerm_pow, coe_pow, SameCycle.exists_pow_eq'', Finset.product_self_eq_disjiUnion_perm, IsCycleOn.pow_apply_eq, Equiv.pow_mulRight
|
ofSubtype 📖 | CompOp | 25 mathmath: subtypePerm_ofSubtype, disjoint_ofSubtype_noncommPiCoprod, disjoint_ofSubtype_of_memFixedPoints_self, ofSubtype_apply_mem_iff_mem, cycleType_ofSubtype, subtypeEquivSubtypePerm_apply_coe, support_ofSubtype, ofSubtype_subtypePerm_of_mem, ofSubtype_apply_of_mem, ofSubtype_subtypePerm, ofSubtype_apply_coe, ofSubtype_eq_iff, ofSubtype_swap_eq, ofSubtype_apply_of_not_mem, ofSubtype_injective, IsCycle.forall_commute_iff, IsCycle.commute_iff, ofSubtype_support_disjoint, IsSwap.of_subtype_isSwap, ofSubtype_mem_stabilizer, ofSubtype_subtypePerm_of_not_mem, OnCycleFactors.kerParam_apply, sign_ofSubtype, zpow_eq_ofSubtype_subtypePerm_iff, commute_ofSubtype_noncommPiCoprod
|
permCongrHom 📖 | CompOp | — |
permGroup 📖 | CompOp | 343 mathmath: Polynomial.Gal.galActionHom_restrict, Fin.sign_cycleIcc_of_eq, DilationEquiv.toPerm_apply, AlternatingMap.domCoprod.summand_mk'', Matrix.det_apply, Polynomial.Gal.galActionHom_bijective_of_prime_degree', alternatingGroup.eq_bot_of_card_le_two, List.form_perm_zpow_apply_mem_imp_mem, smul_def, Basis.toCentralizer_equivariant, alternatingGroup.commutator_perm_eq, MeasureTheory.Measure.QuasiMeasurePreserving.image_zpow_ae_eq, ContinuousMultilinearMap.alternatization_apply_apply, Equiv.zsmul_addLeft, alternatingGroup.isPreprimitive_of_three_le_card, AlternatingMap.map_perm, sign_of_cycleType, Polynomial.Gal.galActionHom_injective, Matrix.det_permute, Set.powersetCard.isPretransitive, disjoint_of_disjoint_support, subtypePerm_ofSubtype, Basis.toCentralizer_apply, RootPairing.reflectionPerm_sq, subtypeCongrHom_injective, cycleOf_self_apply_zpow, disjoint_ofSubtype_noncommPiCoprod, closure_isSwap, exists_mem_stabilizer_smul_eq, OnCycleFactors.mem_range_toPermHom_iff', alternatingGroup.card_two_sylow_of_card_eq_four, AlternatingMap.domCoprod_coe, DomMulAct.mem_stabilizer_iff, alternatingGroup.kleinFour_card_of_card_eq_four, sign_subtypePerm, set_support_zpow_subset, Disjoint.zpow_disjoint_zpow, IsCycle.pow_iff, OnCycleFactors.kerParam_range_card, disjoint_ofSubtype_of_memFixedPoints_self, exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard, OnCycleFactors.kerParam_injective, MonoidHom.toHomPerm_apply_symm_apply, sign_trans_trans_symm, Equiv.swap_smul_involutive, mclosure_swap_castSucc_succ, viaFintypeEmbedding_sign, AlternatingGroup.isPreprimitive_of_three_le_card, ofSubtype_apply_mem_iff_mem, sign_symm, Matrix.permMatrixHom_apply, IsCycle.commute_iff', cycleFactorsFinset_noncommProd, Equiv.altCongrHom_apply_coe, disjoint_closure_of_disjoint_support, Equiv.zpow_mulRight, Fin.sign_cycleRange, sign_eq_prod_prod_Ioi, prod_Ioi_comp_eq_sign_mul_prod, OnCycleFactors.nat_card_range_toPermHom, alternatingGroup.normalClosure_swap_mul_swap_five, zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff, alternatingGroup.subsingleton_two_sylow, mul_mem_alternatingGroup_of_isSwap, cycleFactorsFinset_eq_finset, alternatingGroup.isCoatom_stabilizer_singleton, sign_of_cycleType_eq_replicate, commute_iff_of_mem_cycleFactorsFinset, SameCycle.zpow_right, sumCongrHom.card_range, Set.BijOn.perm_zpow, decomposeFin.symm_sign, cycleType_ofSubtype, RootPairing.weylGroup_apply_root, Rack.envelAction_prop, alternatingGroup.characteristic_kleinFour, mem_closure_isSwap, AlternatingMap.map_congr_perm, zpow_apply_eq_of_apply_apply_eq_self, Set.powersetCard.isPretransitive_alternatingGroup, closure_isCycle, alternatingGroup.kleinFour_isKleinFour, AlternatingGroup.card_of_cycleType_singleton, SameCycle.exists_pow_eq', alternatingGroup.normalClosure_finRotate_five, isConj_of_cycleType_eq, sign_prodExtendRight, isCycle_swap_mul_aux₁, Function.IsFixedPt.perm_zpow, alternatingGroup.kleinFour_eq_commutator, subtypeEquivSubtypePerm_apply_coe, sign_abs, SameCycle.exists_fin_pow_eq, Fin.sign_cycleIcc_of_ge, GrpCat.SurjectiveOfEpiAuxs.g_apply_infinity, GrpCat.SurjectiveOfEpiAuxs.comp_eq, Basis.card_ofPermHom_support, alternatingGroup.center_eq_bot, alternatingGroup.stabilizer.surjective_toPerm, finite_compl_fixedBy_swap, Basis.ofPermHom_apply, zpow_apply_eq_self_of_apply_eq_self, MultilinearMap.domCoprod_alternization_coe, Set.prod_self_eq_iUnion_perm, sign_trans, sameCycle_zpow_right, OnCycleFactors.mem_range_toPermHom'_iff, sign_sumCongr, sign_eq_prod_prod_Iio, swap_mem_stabilizer, card_isConj_eq, Matrix.det_permutation, support_noncommProd, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, closure_cycle_coprime_swap, not_solvable, IsSwap.finite_compl_fixedBy, alternatingGroup.coe_kleinFour_of_card_eq_four, subtypeCongrHom.card_range, viaEmbeddingHom_apply, cycleOf_apply_apply_zpow_self, IsSwap.orderOf, GrpCat.SurjectiveOfEpiAuxs.agree, RegularWreathProduct.toPermInj, Basis.ofPermHom_mem_centralizer, MulAction.toPermHom_apply, sign_bij, support_zpowers_of_mem_cycleFactorsFinset_le, Fin.sign_cycleIcc_of_le, stabilizer_isPreprimitive, applyFaithfulSMul, support_ofSubtype, mem_alternatingGroup, IsCycle.support_pow_eq_iff, Matrix.det_reindex, isConj_swap, support_zpow_le, SameCycle.zpow_left, OnCycleFactors.val_centralizer_smul, Equiv.zpow_mulLeft, sign_refl, IsCycle.orderOf, ofSubtype_subtypePerm_of_mem, lcm_cycleType, swap_mem_closure_isSwap, instCharacteristicPermAlternatingGroup, AlternatingGroup.card_of_cycleType, zpow_apply_mem_support, Basis.toPermHom_apply_toCentralizer, ofSubtype_apply_of_mem, sign_mul, finRotate_bit1_mem_alternatingGroup, centralizer_le_alternating_iff, OnCycleFactors.mem_ker_toPermHom_iff, Basis.ofPermHom_support, mem_sumCongrHom_range_of_perm_mapsTo_inl, alternatingGroup.index_eq_one, IsCycle.exists_zpow_eq, Basis.ofPermHomFun_commute_zpow_apply, sign_symm_trans_trans, mem_ofSign, ofSubtype_subtypePerm, Basis.ofPermHomFun_apply_mem_support_cycle_iff, mem_cycleFactorsFinset_conj', sigmaCongrRightHom_injective, alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four, alternatingGroup.nontrivial_of_three_le_card, ofSubtype_apply_coe, zpow_eq_zpow_on_iff, Equiv.swap_mem_stabilizer, IsCycle.zpowersEquivSupport_apply, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset', MultilinearMap.alternatization_apply, OnCycleFactors.cycleType_kerParam_apply_apply, RootPairing.range_weylGroupToPerm, AlternatingGroup.isMultiplyPretransitive, GrpCat.SurjectiveOfEpiAuxs.h_apply_infinity, alternatingGroup.exists_mem_stabilizer_smul_eq, decomposeOption_symm_sign, alternatingGroup.coe_two_sylow_of_card_eq_four, AddConstEquiv.toPerm_apply, subtypeCongrHom_apply, RootPairing.Equiv.indexHom_apply, AddAction.toPermHom_apply_symm_apply, OnCycleFactors.coe_toPermHom, exists_mem_stabilizer_isThreeCycle, sign_permCongr, eq_top_of_isMultiplyPretransitive, two_mul_card_alternatingGroup, commutator_alternatingGroup_eq_top, sigmaCongrRightHom.card_range, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, instIsPreprimitive, sumCongrHom_injective, swap_mul_swap_same_mem_closure_three_cycles, AlternatingGroup.isPretransitive_of_three_le_card, closure_of_isSwap_of_isPretransitive, card_alternatingGroup, alternatingGroup.stabilizer_isPreprimitive, prod_list_swap_mem_alternatingGroup_iff_even_length, dvd_of_mem_cycleType, two_mul_nat_card_alternatingGroup, fin_5_not_solvable, IsSwap.mul_mem_closure_three_cycles, sigmaCongrRightHom_apply, IsThreeCycle.alternating_normalClosure, IsCycleOn.range_zpow, cycleFactorsFinset_conj_eq, alternatingGroup.normal, alternatingGroup.normal_kleinFour, subgroup_eq_top_of_nontrivial, isConj_of_support_equiv, mem_closure_isSwap', DomMulAct.stabilizerMulEquiv_apply, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset, Matrix.det_mul_aux, IsThreeCycle.orderOf, alternatingGroup.isSimpleGroup_five, OnCycleFactors.mem_range_toPermHom_iff, alternatingGroup.isCoatom_stabilizer, Equiv.zsmul_addRight, Matrix.det_permute', ofSubtype_eq_iff, Polynomial.Gal.galActionHom_bijective_of_prime_degree, OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one, subtypePerm_zpow, ofSubtype_swap_eq, IsCycle.zpowersEquivSupport_symm_apply, Set.powersetCard.isPreprimitive_perm, sameCycle_zpow_left, alternatingGroup.exponent_kleinFour_of_card_eq_four, IsCycleOn.zpow_apply_eq, MultilinearMap.alternatization_coe, Basis.mem_fixedPoints_or_exists_zpow_eq, IsCycleOn.zpow_apply_eq_zpow_apply, ofSubtype_apply_of_not_mem, OnCycleFactors.toPermHom_apply, isConj_iff_cycleType_eq, isCoatom_stabilizer, Set.powersetCard.isPreprimitive_alternatingGroup, alternatingGroup.instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup, iteratedWreathToPermHomInj, closure_cycle_adjacent_swap, ofSubtype_injective, Subgroup.normalCore_eq_ker, Equiv.swap_smul_self_smul, subtypePerm_apply_zpow_of_mem, GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range, sign_extendDomain, alternatingGroup.commutator_perm_le, cycleFactorsFinset_conj, AddAction.toPermHom_apply_apply, alternatingGroup.isPretransitive_of_three_le_card, Basis.ofPermHomFun_mul, instIsPretransitive, IsMultiplyPretransitive.alternatingGroup_le, Polynomial.Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia, AddAction.coe_toPermHom, sign_finRotate, alternatingGroup.isMultiplyPretransitive, IsCycle.sign, sign_inv, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, IsThreeCycle.sign, AlternatingMap.domDomCongr_perm, IsCycle.forall_commute_iff, IsSwap.sign_eq, stabilizer.surjective_toPerm, Polynomial.Splits.surjective_toPermHom_of_iSup_inertia_eq_top, OnCycleFactors.kerParam_range_le_centralizer, sign_prodCongrRight, isCoatom_stabilizer_of_ncard_lt_ncard_compl, Disjoint.orderOf, orderOf_cycleOf_dvd_orderOf, IsCycle.commute_iff, sign_eq_sign_of_equiv, sign_one, eq_top_if_isMultiplyPretransitive, extendDomain_zpow, closure_prime_cycle_swap, sumCongrHom_apply, MonoidHom.toHomPerm_apply_apply, extendDomainHom_apply, ofSubtype_support_disjoint, Matrix.det_apply', sign_prod_list_swap, mclosure_isSwap, pow_mod_orderOf_cycleOf_apply, cycle_zpow_mem_support_iff, moves_in, Disjoint.cycleType_noncommProd, IsSwap.of_subtype_isSwap, cycleOf_zpow_apply_self, partition_eq_of_isConj, sign_prodCongrLeft, alternatingGroup.card_of_card_eq_four, mem_conj_support, disjoint_noncommProd_right, AlternatingGroup.map_subtype_of_cycleType, sign_of_cycleType', sign_subtypeCongr, GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset, AlternatingMap.domCoprod_apply, OnCycleFactors.kerParam_range_eq, nat_card_alternatingGroup, ofSubtype_mem_stabilizer, closure_cycleType_eq_2_2_eq_alternatingGroup, exteriorPower.toTensorPower_apply_ιMulti, prod_Iio_comp_eq_sign_mul_prod, alternatingGroup_eq_sign_ker, SameCycle.exists_pow_eq'', Equiv.optionCongr_sign, MulAction.coe_toPermHom, alternatingGroup.index_eq_two, Basis.ofPermHomFun_one, ofSubtype_subtypePerm_of_not_mem, zpow_apply_comm, commutator_alternatingGroup_eq_self, sign_swap', apply_zpow_apply_eq_iff, IsThreeCycle.mem_alternatingGroup, OnCycleFactors.kerParam_apply, AlternatingGroup.card_of_cycleType_mul_eq, sign_swap, closure_three_cycles_eq_alternating, card_isConj_mul_eq, sign_ofSubtype, nat_card_centralizer, RootPairing.Equiv.indexEquiv_inv, extendDomainHom_injective, IsCycle.isConj_iff, zpow_eq_ofSubtype_subtypePerm_iff, MultilinearMap.alternatization_def, OnCycleFactors.range_toPermHom_eq_range_toPermHom', OnCycleFactors.centralizer_smul_def, sign_surjective, commute_ofSubtype_noncommPiCoprod, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl, OnCycleFactors.sign_kerParam_apply_apply, IsCycle.isConj, AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero, viaEmbeddingHom_injective, isMultiplyPretransitive
|
sigmaCongrRightHom 📖 | CompOp | 3 mathmath: sigmaCongrRightHom_injective, sigmaCongrRightHom.card_range, sigmaCongrRightHom_apply
|
subtypeCongrHom 📖 | CompOp | 3 mathmath: subtypeCongrHom_injective, subtypeCongrHom.card_range, subtypeCongrHom_apply
|
subtypeEquivSubtypePerm 📖 | CompOp | 4 mathmath: subtypeEquivSubtypePerm_apply_coe, subtypeEquivSubtypePerm_apply_of_mem, subtypeEquivSubtypePerm_apply_of_not_mem, subtypeEquivSubtypePerm_symm_apply
|
subtypePerm 📖 | CompOp | 27 mathmath: subtypePerm_mul, subtypePerm_ofSubtype, IsCycleOn.isCycle_subtypePerm, sign_subtypePerm, subtypePerm_inv, IsCycle.commute_iff', commute_iff_of_mem_cycleFactorsFinset, ofSubtype_subtypePerm_of_mem, ofSubtype_subtypePerm, subtypePerm_apply_pow_of_mem, inv_subtypePerm, subtypePerm_on_cycleFactorsFinset, SameCycle.subtypePerm, ofSubtype_eq_iff, subtypePerm_zpow, sameCycle_subtypePerm, subtypePerm_apply_zpow_of_mem, IsCycle.forall_commute_iff, subtypeEquivSubtypePerm_symm_apply, IsCycle.commute_iff, IsCycleOn.subtypePerm, subtypePerm_apply, subtypePerm_pow, subtypePerm_one, support_subtypePerm, ofSubtype_subtypePerm_of_not_mem, zpow_eq_ofSubtype_subtypePerm_iff
|
sumCongrHom 📖 | CompOp | 8 mathmath: AlternatingMap.domCoprod.summand_mk'', AlternatingMap.domCoprod_coe, sumCongrHom.card_range, mem_sumCongrHom_range_of_perm_mapsTo_inl, sumCongrHom_injective, sumCongrHom_apply, AlternatingMap.domCoprod_apply, AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero
|