| Name | Category | Theorems |
|---|
arrowProdEquivProdArrow 📖 | CompOp | 2 mathmath: arrowProdEquivProdArrow_apply, arrowProdEquivProdArrow_symm_apply
|
boolArrowEquivProd 📖 | CompOp | 3 mathmath: boolArrowEquivProd_symm_apply, boolArrowEquivProd_apply, Finset.finsetCongr_piAntidiag_eq_antidiag
|
boolProdEquivSum 📖 | CompOp | 2 mathmath: boolProdEquivSum_symm_apply, boolProdEquivSum_apply
|
curry 📖 | CompOp | 4 mathmath: measurable_equivCurry_symm, curry_apply, measurable_equivCurry, curry_symm_apply
|
emptyProd 📖 | CompOp | — |
funSplitAt 📖 | CompOp | 2 mathmath: funSplitAt_symm_apply, funSplitAt_apply
|
pemptyProd 📖 | CompOp | — |
piEquivPiSubtypeProd 📖 | CompOp | 5 mathmath: piEquivPiSubtypeProd_symm_apply, measurable_piEquivPiSubtypeProd_symm, preimage_piEquivPiSubtypeProd_symm_pi, piEquivPiSubtypeProd_apply, measurable_piEquivPiSubtypeProd
|
piSplitAt 📖 | CompOp | 2 mathmath: piSplitAt_symm_apply, piSplitAt_apply
|
pprodCongr 📖 | CompOp | 2 mathmath: pprodCongr_symm_apply, pprodCongr_apply
|
pprodEquivProd 📖 | CompOp | 2 mathmath: pprodEquivProd_apply, pprodEquivProd_symm_apply
|
pprodEquivProdPLift 📖 | CompOp | 2 mathmath: pprodEquivProdPLift_apply, pprodEquivProdPLift_symm_apply
|
pprodProd 📖 | CompOp | 2 mathmath: pprodProd_apply, pprodProd_symm_apply
|
prodAssoc 📖 | CompOp | 27 mathmath: contDiff_prodAssoc_symm, ContinuousLinearEquiv.coe_prodAssoc, Homeomorph.prodAssoc_toEquiv, prod_assoc_image, Matrix.kroneckerTMul_assoc', Matrix.kroneckerMap_assoc₁, contDiff_prodAssoc, Filter.tendsto_prodAssoc_symm, TensorProduct.toMatrix_assoc, prodAssoc_apply, AddEquiv.coe_prodAssoc, MulEquiv.coe_prodAssoc, LinearIsometryEquiv.coe_prodAssoc_symm, Matrix.kronecker_assoc, Matrix.kronecker_assoc', AddEquiv.coe_prodAssoc_symm, Filter.tendsto_prodAssoc, MulEquiv.coe_prodAssoc_symm, Filter.prod_assoc, Filter.prod_assoc_symm, Matrix.kroneckerMap_assoc, prodAssoc_symm_apply, prod_assoc_preimage, prod_assoc_symm_image, Matrix.kroneckerTMul_assoc, prod_assoc_symm_preimage, LinearIsometryEquiv.coe_prodAssoc
|
prodComm 📖 | CompOp | 17 mathmath: Matrix.natCast_kronecker, Matrix.one_kronecker, Nat.map_swap_divisorsAntidiagonal, Int.map_prodComm_divisorsAntidiag, prodComm_apply, Matrix.diagonal_kroneckerTMul, prodCongrRight_trans_prodComm, prodComm_symm, coe_prodComm, prodCongrLeft_trans_prodComm, Matrix.diagonal_kronecker, Rep.leftRegularTensorTrivialIsoFree_inv_hom, Matrix.ofNat_kronecker, Matrix.comp_diagonal, Rep.leftRegularTensorTrivialIsoFree_hom_hom, Matrix.kroneckerMap_diagonal_left, Finset.map_prodComm_antidiagonal
|
prodCongr 📖 | CompOp | 10 mathmath: prodCongr_refl_right, CategoryTheory.Functor.Monoidal.RepresentableBy.tensorObj_homEquiv, Matrix.kroneckerMap_reindex_right, Matrix.kroneckerMap_reindex, AlgEquiv.prodCongr_apply, prodCongr_refl_left, prodCongr_apply, Matrix.kroneckerMap_reindex_left, prodCongr_symm, AlgEquiv.prodCongr_symm_apply
|
prodCongrLeft 📖 | CompOp | 8 mathmath: prodCongrLeft_apply_snd, prodCongr_refl_right, prodCongrLeft_apply_fst, prodCongrRight_trans_prodComm, prodCongrLeft_trans_prodComm, prodCongrLeft_symm, prodCongrLeft_apply, Perm.sign_prodCongrLeft
|
prodCongrRight 📖 | CompOp | 11 mathmath: sigmaCongrRight_sigmaEquivProd, prodCongr_refl_left, prodCongrRight_trans_prodComm, prodCongrLeft_trans_prodComm, prodCongrRight_apply_snd, sigmaEquivProd_sigmaCongrRight, prodCongrRight_apply_fst, Perm.sign_prodCongrRight, prodCongrRight_symm, Perm.prod_prodExtendRight, prodCongrRight_apply
|
prodEmpty 📖 | CompOp | — |
prodPEmpty 📖 | CompOp | — |
prodPProd 📖 | CompOp | 2 mathmath: prodPProd_apply, prodPProd_symm_apply
|
prodPUnit 📖 | CompOp | 2 mathmath: prodPUnit_apply, prodPUnit_symm_apply
|
prodPiEquivSumPi 📖 | CompOp | 2 mathmath: prodPiEquivSumPi_apply, prodPiEquivSumPi_symm_apply
|
prodProdProdComm 📖 | CompOp | 8 mathmath: Set.graphOn_prod_graphOn, AddEquiv.prodProdProdComm_toEquiv, MulEquiv.prodProdProdComm_toEquiv, prodProdProdComm_symm, ContinuousLinearEquiv.coe_prodProdProdComm, prodProdProdComm_apply, Set.graphOn_prod_prodMap, RingEquiv.prodProdProdComm_toEquiv
|
prodShear 📖 | CompOp | 2 mathmath: prodShear_apply, prodShear_symm_apply
|
prodSubtypeFstEquivSubtypeProd 📖 | CompOp | 1 mathmath: Matrix.comp_toSquareBlock
|
prodUnique 📖 | CompOp | 5 mathmath: prodUnique_symm_apply, LinearEquiv.coe_prodUnique, prodUnique_apply, coe_prodUnique, ContinuousLinearEquiv.coe_prodUnique
|
punitProd 📖 | CompOp | 3 mathmath: punitProd_symm_apply, punitProd_apply, HahnSeries.SummableFamily.smul_eq
|
sigmaPUnit 📖 | CompOp | 3 mathmath: sigmaPUnit_symm_apply_snd, sigmaPUnit_symm_apply_fst, sigmaPUnit_apply
|
sigmaProdDistrib 📖 | CompOp | 3 mathmath: sigmaProdDistrib_symm_apply, Homeomorph.toEquiv_sigmaProdDistrib, sigmaProdDistrib_apply
|
sigmaUnique 📖 | CompOp | 3 mathmath: sigmaUnique_apply, sigmaUnique_symm_apply, coe_sigmaUnique
|
subtypeProdEquivProd 📖 | CompOp | — |
subtypeProdEquivSigmaSubtype 📖 | CompOp | — |
sumArrowEquivProdArrow 📖 | CompOp | 8 mathmath: AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr, sumArrowEquivProdArrow_symm_apply_inr, RingEquiv.sumArrowEquivProdArrow_symm_apply, sumArrowEquivProdArrow_apply_fst, RingEquiv.sumArrowEquivProdArrow_apply, sumArrowEquivProdArrow_apply_snd, sumArrowEquivProdArrow_symm_apply_inl, AlgEquiv.sumArrowEquivProdArrow_apply
|
sumPiEquivProdPi 📖 | CompOp | 11 mathmath: prodPiEquivSumPi_apply, sumPiEquivProdPi_symm_apply, MeasurableEquiv.coe_sumPiEquivProdPi, LinearEquiv.sumPiEquivProdPi_apply, sumPiEquivProdPi_symm_preimage_univ_pi, piCongrLeft_sumInl, LinearEquiv.sumPiEquivProdPi_symm_apply, prodPiEquivSumPi_symm_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm, piCongrLeft_sumInr, sumPiEquivProdPi_apply
|
sumProdDistrib 📖 | CompOp | 11 mathmath: Homeomorph.sumProdDistrib_symm_apply, Prod.Lex.sumLexProdLexDistrib_symm_apply, sumProdDistrib_symm_apply_right, Prod.Lex.sumLexProdLexDistrib_apply, Homeomorph.sumProdDistrib_apply, sumProdDistrib_apply_left, sumProdDistrib_apply_right, sumProdDistrib_symm_apply_left, SimpleGraph.Iso.boxProdSumDistrib_symm_apply, SimpleGraph.Iso.boxProdSumDistrib_apply, SimpleGraph.Iso.sumBoxProdDistrib_toEquiv
|
uniqueProd 📖 | CompOp | 5 mathmath: uniqueProd_symm_apply, ContinuousLinearEquiv.coe_uniqueProd, LinearEquiv.coe_uniqueProd, uniqueProd_apply, coe_uniqueProd
|
uniqueSigma 📖 | CompOp | 2 mathmath: uniqueSigma_apply, uniqueSigma_symm_apply
|