| Name | Category | Theorems |
|---|
diag 📖 | CompOp | 21 mathmath: diag_union, prod_diag, diag_card, image_diag, Sym2.filter_image_mk_isDiag, sum_diag, diag_union_offDiag, Sym2.card_image_diag, mem_diag, product_sdiff_diag, diag_eq_empty, image_diag_union_image_offDiag, diag_inter, product_sdiff_offDiag, diag_mono, disjoint_diag_offDiag, diag_insert, diag_nonempty, diag_singleton, diag_eq_filter, diag_empty
|
instSProd 📖 | CompOp | 180 mathmath: WittVector.remainder_vars, sup_add_sup, Set.Finite.toFinset_prod, addEnergy_eq_sum_sq', Nat.smoothNumbersUpTo_subset_image, sup_product_right, product_biUnion, image₂_curry, SupIndep.product, product_union, product_image_fst, subset_product_image_snd, empty_product, inf'_sup_inf', Rel.interedges_biUnion, image_uncurry_product, product_pow, product_singleton, le_addRothNumber_product, disjUnion_product, image_smul_product, filter_product_right, map_consEquiv_filter_piFinset, prodMk_sup'_sup', Sym2.filter_image_mk_isDiag, UniqueMul.exists_iff_exists_existsUnique, map_snocEquiv_filter_piFinset, Rel.card_interedges_finpartition, image_div_product, image_swap_product, product_inter, product_image_snd, union_product, card_product, inf_prodMap, singleton_product_singleton, SimpleGraph.neighborFinset_completeEquipartiteGraph, product_subset_product, wittStructureRat_vars, addEnergy_eq_sum_sq, zero_product_zero, mulEnergy_eq_sum_sq', filter_product_card, product_subset_product_left, TwoUniqueProds.uniqueMul_of_one_lt_card, product_eq_biUnion, diag_union_offDiag, sup_product_left, UniqueMul.iff_existsUnique, uIcc_product_uIcc, offDiag_union, div_def, product_eq_sprod, WittVector.wittZSMul_vars, card_mul_inv_eq_convolution_inv, SimpleGraph.neighborFinset_boxProd, prod_product_right', product_sdiff_diag, univ_product_univ, Real.pow_mul_norm_iteratedFDeriv_fourier_le, inf_product_left, filter_piFinset_eq_map_consEquiv, DirectSum.coe_mul_apply, Filter.tendsto_finset_prod_atTop, Nonempty.product, mk_mem_product, SimpleGraph.interedges_def, TwoUniqueSums.uniqueAdd_of_one_lt_card, image_sub_product, inf_product_right, product_disjUnion, UniqueAdd.exists_iff_exists_existsUnique, WittVector.mul_polyOfInterest_vars, filter_piFinset_eq_map_insertNthEquiv, sup_prodMap, inv_product, sup'_inf_sup', WittVector.wittAdd_vars, uIcc_prod_def, product_eq_empty, image_sdiff_product, neg_product, product_eq_biUnion_right, ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter, sum_product', card_sq_le_card_mul_mulEnergy, product_nsmul, UniqueMul.iff_card_le_one, SimpleGraph.unreduced_edges_subset, EMetric.pair_reduction, subset_product_image_fst, prod_product_right, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, image_add_product, product_eq_univ, sum_product_right', expect_product, le_mulRothNumber_product, wittStructureInt_vars, product_val, prodMap_map_product, prodMap_image_product, card_sq_le_card_mul_addEnergy, Ici_prod_def, offDiag_insert, SimpleGraph.triangle_counting', prodMk_inf'_inf', Icc_prod_def, product_mul_product_comm, prod_product, sub_def, WittVector.wittSub_vars, disjoint_product, Finpartition.IsEquipartition.sum_nonUniforms_lt, YoungDiagram.row_eq_prod, image_sup_product, map_insertNthEquiv_filter_piFinset, WittVector.wittPow_vars, smul_def, mulEnergy_eq_sum_sq, Ici_product_Ici, Sym2.filter_image_mk_not_isDiag, Nat.divisorsAntidiagonal_eq_prod_filter_of_le, UniqueAdd.iff_card_le_one, filter_piFinset_eq_map_snocEquiv, nontrivial_prod_iff, WittVector.polyOfInterest_vars, Real.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, DirectSum.mul_eq_sum_support_ghas_mul, image_mul_product, inf_sup_inf, product_sdiff_offDiag, coe_product, map_swap_product, product_empty, image₂_mk_eq_product, nonempty_product, sup_inf_sup, YoungDiagram.col_eq_prod, SimpleGraph.interedges_biUnion, WittVector.wittNSMul_vars, singleton_product, Iic_product_Iic, product_subset_product_right, subset_product, mul_def, Icc_product_Icc, sum_product_right, Nat.card_pair_lcm_eq, one_product_one, addEnergy_eq_card_filter, sum_product, mulEnergy_eq_card_filter, add_def, PairReduction.pairSet_subset, mem_product, Iic_prod_def, product_add_product_comm, inter_product, prod_product', diag_eq_filter, product_self_eq_disjiUnion_perm, filter_product, product_inter_product, WittVector.wittNeg_vars, vadd_def, card_add_neg_eq_addConvolution_neg, filter_product_left, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, image_vadd_product, UniqueAdd.iff_existsUnique, WittVector.wittPolyProd_vars, Multiset.toEnumFinset_filter_eq, Set.toFinset_prod, sym2_eq_image, expect_product', WittVector.wittPolyProdRemainder_vars, Finpartition.parts_inf, WittVector.wittMul_vars, image_inf_product
|
offDiag 📖 | CompOp | 29 mathmath: SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq, Finpartition.IsEquipartition.card_biUnion_offDiag_le', Finpartition.IsEquipartition.card_biUnion_offDiag_le, Set.Finset.coe_einfsep, offDiag_card, offDiag_singleton, coe_offDiag, diag_union_offDiag, offDiag_union, offDiag_mono, product_sdiff_diag, Set.toFinset_offDiag, coe_infsep, Finpartition.coe_energy, SimpleGraph.unreduced_edges_subset, Set.Finite.toFinset_offDiag, Set.toFinset_off_diag, offDiag_insert, image_diag_union_image_offDiag, Sym2.filter_image_mk_not_isDiag, product_sdiff_offDiag, Sym2.card_image_offDiag, offDiag_empty, mem_offDiag, disjoint_diag_offDiag, sum_sym2_filter_not_isDiag, offDiag_filter_lt_eq_filter_le, Sym2.two_mul_card_image_offDiag, offDiag_inter
|
product 📖 | CompOp | 4 mathmath: product_eq_sprod, SzemerediRegularity.edgeDensity_chunk_uniform, supIndep_product_iff, SzemerediRegularity.edgeDensity_chunk_not_uniform
|