| Name | Category | Theorems |
|---|
intEquivNatSumNat 📖 | CompOp | — |
natEquivNatSumPUnit 📖 | CompOp | — |
natSumPUnitEquivNat 📖 | CompOp | — |
ofFiberEquiv 📖 | CompOp | 3 mathmath: ofFiberEquiv_map, ofFiberEquiv_apply, ofFiberEquiv_symm_apply
|
piComm 📖 | CompOp | 2 mathmath: piComm_apply, piComm_symm
|
piCongr 📖 | CompOp | 3 mathmath: piCongr_apply_apply, piCongr_symm_apply, coe_piCongr_symm
|
piCongr' 📖 | CompOp | 3 mathmath: piCongr'_symm_apply_symm_apply, coe_piCongr', piCongr'_apply
|
piCongrFiberwise 📖 | CompOp | 2 mathmath: piCongrFiberwise_apply, piCongrFiberwise_symm_apply
|
piCongrLeft 📖 | CompOp | 26 mathmath: Homeomorph.piCongr_apply, piCongrLeft_apply, Homeomorph.toEquiv_piCongr, Homeomorph.toEquiv_piCongrLeft, piCongrLeft_preimage_univ_pi, piCongrLeft_symm_apply, Finset.piCongrLeft_comp_restrict, piCongrLeft_preimage_pi, piCongrLeft_symm_preimage_univ_pi, piCongrLeft_symm_preimage_pi, AlgEquiv.piCongrLeft_apply, piCongrLeft_sumInl, MeasurableEquiv.coe_piCongrLeft, UniformEquiv.piCongrLeft_toEquiv, UniformEquiv.piCongr_toEquiv, piCongrLeft_apply_eq_cast, Set.piCongrLeft_comp_restrict, piCongrLeft_sumInr, AlgEquiv.piCongrLeft_symm_apply, piCongrLeft_apply_apply, UniformEquiv.piCongr_apply, Finset.restrict_comp_piCongrLeft, Preorder.piCongrLeft_comp_restrictLe, piCongrLeft_refl, Preorder.piCongrLeft_comp_frestrictLe, measurable_piCongrLeft
|
piCongrLeft' 📖 | CompOp | 15 mathmath: MultilinearMap.domDomCongrLinearEquiv'_symm_apply, Function.piCongrLeft'_symm_update, LinearIsometryEquiv.piLpCongrLeft_apply, AlgEquiv.piCongrLeft'_apply, Homeomorph.piCongrLeft_apply, Function.piCongrLeft'_update, LinearEquiv.piCongrLeft'_symm_apply, MultilinearMap.domDomCongrLinearEquiv'_apply, piCongrLeft'_symm, piCongrLeft'_symm_apply, piCongrLeft'_symm_apply_apply, piCongrLeft'_refl, UniformEquiv.piCongrLeft_apply, AlgEquiv.piCongrLeft'_symm_apply, piCongrLeft'_apply
|
piCongrRight 📖 | CompOp | 9 mathmath: Homeomorph.piCongr_apply, Homeomorph.toEquiv_piCongr, piCongrRight_symm_apply, Homeomorph.toEquiv_piCongrRight, UniformEquiv.piCongr_toEquiv, piCongrRight_apply, UniformEquiv.piCongr_apply, piCongrRight_refl, UniformEquiv.piCongrRight_toEquiv
|
piCongrSet 📖 | CompOp | 2 mathmath: piCongrSet_apply, piCongrSet_symm_apply
|
piCongrSigmaFiber 📖 | CompOp | 2 mathmath: piCongrSigmaFiber_symm_apply, piCongrSigmaFiber_apply
|
piCurry 📖 | CompOp | 4 mathmath: measurable_piCurry_symm, piCurry_apply, piCurry_symm_apply, measurable_piCurry
|
piEquivSubtypeSigma 📖 | CompOp | — |
piOptionEquivProd 📖 | CompOp | 2 mathmath: piOptionEquivProd_symm_apply, piOptionEquivProd_apply
|
punitOfNonemptyOfSubsingleton 📖 | CompOp | — |
setValue 📖 | CompOp | 1 mathmath: setValue_eq
|
sigmaAssocProd 📖 | CompOp | 5 mathmath: sigmaAssocProd_apply_fst, sigmaAssocProd_apply_snd_snd, sigmaAssocProd_apply_snd_fst, sigmaAssocProd_symm_apply_snd, sigmaAssocProd_symm_apply_fst
|
sigmaNatSucc 📖 | CompOp | — |
sigmaOptionEquivOfSome 📖 | CompOp | — |
sigmaSigmaSubtype 📖 | CompOp | 2 mathmath: sigmaSigmaSubtype_symm_apply, sigmaSigmaSubtype_apply
|
sigmaSigmaSubtypeEq 📖 | CompOp | 2 mathmath: sigmaSigmaSubtypeEq_apply, sigmaSigmaSubtypeEq_symm_apply
|
sigmaSubtype 📖 | CompOp | 3 mathmath: sigmaSubtype_symm_apply_coe_snd, sigmaSubtype_apply, sigmaSubtype_symm_apply_coe_fst
|
sigmaSubtypeEquivOfSubset 📖 | CompOp | — |
sigmaSubtypeFiberEquiv 📖 | CompOp | — |
sigmaSubtypeFiberEquivSubtype 📖 | CompOp | — |
subtypeCongr 📖 | CompOp | — |
subtypeEquiv 📖 | CompOp | 8 mathmath: subtypeEquiv_trans, subtypeEquiv_apply, AffineBasis.basisOf_reindex, sigmaSigmaSubtype_apply, Homeomorph.subtype_toEquiv, subtypeEquiv_refl, coe_subtypeEquiv_eq_map, subtypeEquiv_symm
|
subtypeEquivCodomain 📖 | CompOp | 6 mathmath: subtypeEquivCodomain_symm_apply, coe_subtypeEquivCodomain_symm, subtypeEquivCodomain_apply, subtypeEquivCodomain_symm_apply_eq, subtypeEquivCodomain_symm_apply_ne, coe_subtypeEquivCodomain
|
subtypeEquivOfSubtype 📖 | CompOp | — |
subtypeEquivOfSubtype' 📖 | CompOp | — |
subtypeEquivProp 📖 | CompOp | 2 mathmath: AlgebraicGeometry.coe_opensRestrict_symm_apply, Homeomorph.ofEqSubtypes_toEquiv
|
subtypeEquivRight 📖 | CompOp | 4 mathmath: subtypeEquivRight_apply_coe, subtypeEquivRight_apply, subtypeEquivRight_symm_apply, subtypeEquivRight_symm_apply_coe
|
subtypePiEquivPi 📖 | CompOp | — |
subtypePreimage 📖 | CompOp | 4 mathmath: subtypePreimage_apply, subtypePreimage_symm_apply_coe_pos, subtypePreimage_symm_apply_coe_neg, subtypePreimage_symm_apply_coe
|
subtypeQuotientEquivQuotientSubtype 📖 | CompOp | 2 mathmath: subtypeQuotientEquivQuotientSubtype_mk, subtypeQuotientEquivQuotientSubtype_symm_mk
|
subtypeSigmaEquiv 📖 | CompOp | — |
subtypeSubtypeEquivSubtype 📖 | CompOp | 2 mathmath: subtypeSubtypeEquivSubtype_apply_coe, subtypeSubtypeEquivSubtype_symm_apply_coe_coe
|
subtypeSubtypeEquivSubtypeExists 📖 | CompOp | 2 mathmath: subtypeSubtypeEquivSubtypeExists_apply_coe, subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe
|
subtypeSubtypeEquivSubtypeInter 📖 | CompOp | 2 mathmath: subtypeSubtypeEquivSubtypeInter_apply_coe, subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe
|
subtypeUnivEquiv 📖 | CompOp | 2 mathmath: subtypeUnivEquiv_apply, subtypeUnivEquiv_symm_apply
|
swap 📖 | CompOp | 103 mathmath: Perm.decomposeFin_symm_of_refl, image_swap_of_mem_of_notMem, Perm.sumCongr_swap_refl, Perm.card_support_swap_mul, apply_swap_eq_self, map_equiv_removeNone, Pi.colex_asc, swap_apply_apply, comp_swap_eq_update, swap_apply_self, Perm.signAux_swap, swap_mul_self, swap_smul_involutive, Perm.mclosure_swap_castSucc_succ, Perm.IsCycle.eq_swap_of_apply_apply_eq_self, swap_comm, Perm.decomposeFin_symm_apply_one, alternatingGroup.normalClosure_swap_mul_swap_five, Perm.support_swap_mul_eq, Perm.support_swap_mul_swap, Perm.cycleType_swap_mul_swap_of_nodup, Perm.disjoint_swap_swap, swap_eq_one_iff, Perm.isCycle_swap_mul_aux₁, finite_compl_fixedBy_swap, Function.Injective.map_swap, swap_comp_apply, Perm.support_swap_iff, Function.Embedding.swap_apply, Perm.swap_mem_stabilizer, swap_mul_involutive, Perm.closure_cycle_coprime_swap, symm_swap, List.formPerm_pair, Pi.lex_desc, swap_apply_def, mul_swap_eq_swap_mul, swap_mul_eq_iff, optionCongr_swap, Perm.isConj_swap, Fin.succAbove_cycleRange, swap_mem_closure_isSwap, mul_swap_involutive, Perm.sumCongr_swap_one, swap_mul_eq_mul_swap, swap_apply_of_ne_of_ne, Perm.IsThreeCycle.eq_swap_mul_swap_iff_mem_support, Perm.signAux3_mul_and_swap, Perm.decomposeFin_symm_apply_succ, swap_inv, List.zipWith_swap_prod_support', Perm.isCycle_swap_mul_aux₂, Perm.sumCongr_one_swap, Perm.support_swap_mul_ge_support_diff, Perm.card_support_swap, symm_trans_swap_trans, mul_swap_mul_self, swap_mem_stabilizer, trans_swap_trans_symm, swap_apply_eq_iff, mul_swap_eq_iff, swap_eq_update, bijOn_swap, swap_mul_swap_mul_swap, Perm.swap_mul_swap_same_mem_closure_three_cycles, Perm.isCycleOn_swap, Matrix.swap_mulVec, Perm.decomposeFin_symm_of_one, swap_self, Function.Injective.swap_apply, Perm.isCycle_swap, Perm.ofSubtype_swap_eq, swap_mul_self_mul, Perm.swap_isSwap_iff, Perm.IsCycle.swap_mul, Perm.closure_cycle_adjacent_swap, swap_injective_of_left, swap_smul_self_smul, Perm.support_swap, List.formPerm_cons_cons, AlternatingMap.map_swap, Perm.sumCongr_refl_swap, alternatingGroup.isConj_swap_mul_swap_of_cycleType_two, AlternatingMap.map_swap_add, Perm.decomposeOption_symm_apply, swap_bijOn_exchange, AlternatingMap.map_add_swap, List.zipWith_swap_prod_support, swap_apply_right, PEquiv.toMatrix_swap, swap_apply_left, swap_bijOn_self, Perm.sign_swap', swap_swap, Function.Injective.swap_comp, Perm.sign_swap, swap_injective_of_right, Perm.isThreeCycle_swap_mul_swap_same, Matrix.vecMul_swap, List.formPerm_append_pair, Function.Embedding.swap_comp, swap_eq_refl_iff, AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero
|
swapCore 📖 | CompOp | 3 mathmath: swapCore_comm, swapCore_self, swapCore_swapCore
|
uniqueCongr 📖 | CompOp | — |