| Metric | Count |
|---|
Definitionsadd, addCommMonoid, addCommSemigroup, addMonoid, addSemigroup, addZeroClass, coeAddMonoidHom, coeMonoidHom, commMonoid, commSemigroup, div, divisionCommMonoid, divisionMonoid, imageAddHom, imageAddMonoidHom, imageMonoidHom, imageMulHom, imageOneHom, imageZeroHom, inv, monoid, mul, mulOneClass, neg, npow, nsmul, one, semigroup, singletonAddHom, singletonAddMonoidHom, singletonMonoidHom, singletonMulHom, singletonOneHom, singletonZeroHom, sub, subtractionCommMonoid, subtractionMonoid, zero, zpow, zsmul, instFintypeOne, instFintypeZero | 42 |
Theoremsadd, card_nsmul_mono, card_pow_mono, div, inv, mul, neg, nsmul, of_add_left, of_add_right, of_div_left, of_div_right, of_inv, of_mul_left, of_mul_right, of_neg, of_sub_left, of_sub_right, one_mem_div, pow, sub, subset_one_iff, subset_zero_iff, zero_mem_sub, zpow, zsmul, add, add_left, add_right, mul, mul_left, mul_right, nsmul, pow, add_def, add_empty, add_eq_empty, add_eq_zero_iff, add_inter_subset, add_mem_add, add_nonempty, add_subset_add, add_subset_add_left, add_subset_add_right, add_subset_iff, add_union, add_univ_of_zero_mem, card_add_iff, card_add_le, card_add_singleton, card_div_le, card_inv, card_inv_le, card_le_card_add_left, card_le_card_add_left_of_injective, card_le_card_add_right, card_le_card_add_right_of_injective, card_le_card_add_self, card_le_card_add_self', card_le_card_div_left, card_le_card_div_right, card_le_card_div_self, card_le_card_mul_left, card_le_card_mul_left_of_injective, card_le_card_mul_right, card_le_card_mul_right_of_injective, card_le_card_mul_self, card_le_card_mul_self', card_le_card_nsmul, card_le_card_pow, card_le_card_sub_left, card_le_card_sub_right, card_le_card_sub_self, card_mul_iff, card_mul_le, card_mul_singleton, card_neg, card_neg_le, card_nsmul_le, card_nsmul_mono, card_one, card_pow_le, card_pow_mono, card_singleton_add, card_singleton_mul, card_sub_le, card_zero, coeAddMonoidHom_apply, coeMonoidHom_apply, coe_add, coe_coeAddMonoidHom, coe_coeMonoidHom, coe_div, coe_eq_one, coe_eq_zero, coe_inv, coe_list_prod, coe_list_sum, coe_mul, coe_neg, coe_nsmul, coe_one, coe_pow, coe_singletonAddHom, coe_singletonAddMonoidHom, coe_singletonMonoidHom, coe_singletonMulHom, coe_singletonOneHom, coe_singletonZeroHom, coe_sub, coe_zero, coe_zpow, coe_zsmul, div_def, div_empty, div_eq_empty, div_inter_subset, div_mem_div, div_nonempty, div_singleton, div_subset_div, div_subset_div_left, div_subset_div_right, div_subset_iff, div_union, empty_add, empty_div, empty_mul, empty_pow, empty_sub, empty_zpow, imageAddHom_apply, imageAddMonoidHom_apply, imageMonoidHom_apply, imageMulHom_apply, imageOneHom_apply, imageZeroHom_apply, image_add, image_add_left, image_add_left', image_add_product, image_add_right, image_add_right', image_div, image_div_product, image_inv, image_inv_eq_inv, image_mul, image_mul_left, image_mul_left', image_mul_product, image_mul_right, image_mul_right', image_neg, image_neg_eq_neg, image_nsmul, image_nsmul_of_ne_zero, image_one, image_op_add, image_op_inv, image_op_mul, image_op_neg, image_op_nsmul, image_op_one, image_op_pow, image_op_zero, image_pow, image_pow_of_ne_zero, image_sub_product, image_zero, inf'_inv, inf'_neg, inf'_one, inf'_zero, inf_add_left, inf_add_right, inf_div_left, inf_div_right, inf_inv, inf_mul_left, inf_mul_right, inf_neg, inf_one, inf_sub_left, inf_sub_right, inf_zero, instAddLeftMono, instAddRightMono, instMulLeftMono, instMulRightMono, inter_add_singleton, inter_add_subset, inter_add_union_subset, inter_add_union_subset_union, inter_div_subset, inter_div_union_subset_union, inter_mul_singleton, inter_mul_subset, inter_mul_union_subset, inter_mul_union_subset_union, inter_nsmul_subset, inter_pow_subset, inter_sub_subset, inter_sub_union_subset_union, inv_def, inv_empty, inv_eq_empty, inv_filter, inv_filter_univ, inv_insert, inv_inter, inv_mem_inv, inv_nonempty_iff, inv_product, inv_singleton, inv_subset_div_right, inv_subset_inv, inv_univ, isAddUnit_coe, isAddUnit_iff, isAddUnit_singleton, isUnit_coe, isUnit_iff, isUnit_iff_singleton, isUnit_iff_singleton_aux, isUnit_singleton, le_inf_add, le_inf_div, le_inf_mul, le_inf_sub, map_one, map_op_add, map_op_inv, map_op_mul, map_op_neg, map_op_nsmul, map_op_one, map_op_pow, map_op_zero, map_zero, max'_one, max'_zero, max_one, max_zero, mem_add, mem_div, mem_inv, mem_inv', mem_mul, mem_neg, mem_neg', mem_nsmul, mem_one, mem_pow, mem_prod_list_ofFn, mem_sub, mem_sum_list_ofFn, mem_zero, min'_one, min'_zero, min_one, min_zero, mul_def, mul_empty, mul_eq_empty, mul_eq_one_iff, mul_inter_subset, mul_mem_mul, mul_nonempty, mul_subset_iff, mul_subset_mul, mul_subset_mul_left, mul_subset_mul_right, mul_union, mul_univ_of_one_mem, neg_def, neg_empty, neg_eq_empty, neg_filter, neg_filter_univ, neg_insert, neg_inter, neg_mem_neg, neg_nonempty_iff, neg_product, neg_singleton, neg_subset_neg, neg_subset_sub_right, neg_univ, nsmul_empty, nsmul_eq_empty, nsmul_mem_nsmul, nsmul_right_monotone, nsmul_singleton, nsmul_subset_nsmul, nsmul_subset_nsmul_add_of_sq_subset_add, nsmul_subset_nsmul_left, nsmul_subset_nsmul_right, nsmul_univ, one_mem_div_iff, one_mem_inv_mul_iff, one_mem_one, one_mem_pow, one_nonempty, one_notMem_div_iff, one_notMem_inv_mul_iff, one_product_one, one_subset, pow_eq_empty, pow_mem_pow, pow_right_monotone, pow_subset_pow, pow_subset_pow_left, pow_subset_pow_mul_of_sq_subset_mul, pow_subset_pow_right, preimage_add_left_singleton, preimage_add_left_zero, preimage_add_left_zero', preimage_add_right_singleton, preimage_add_right_zero, preimage_add_right_zero', preimage_inv, preimage_mul_left_one, preimage_mul_left_one', preimage_mul_left_singleton, preimage_mul_right_one, preimage_mul_right_one', preimage_mul_right_singleton, preimage_neg, product_add_product_comm, product_mul_product_comm, product_nsmul, product_pow, singletonAddHom_apply, singletonAddMonoidHom_apply, singletonMonoidHom_apply, singletonMulHom_apply, singletonOneHom_apply, singletonZeroHom_apply, singleton_add_inter, singleton_add_singleton, singleton_div, singleton_div_singleton, singleton_mul_inter, singleton_mul_singleton, singleton_one, singleton_pow, singleton_sub, singleton_sub_singleton, singleton_zero, singleton_zpow, sub_def, sub_empty, sub_eq_empty, sub_inter_subset, sub_mem_sub, sub_nonempty, sub_singleton, sub_subset_iff, sub_subset_sub, sub_subset_sub_left, sub_subset_sub_right, sub_union, subset_add, subset_add_left, subset_add_right, subset_div, subset_div_left, subset_mul, subset_mul_left, subset_mul_right, subset_nsmul, subset_one_iff_eq, subset_pow, subset_sub, subset_sub_left, subset_zero_iff_eq, sup'_inv, sup'_neg, sup'_one, sup'_zero, sup_add_le, sup_add_left, sup_add_right, sup_div_le, sup_div_left, sup_div_right, sup_inv, sup_mul_le, sup_mul_left, sup_mul_right, sup_neg, sup_one, sup_sub_le, sup_sub_left, sup_sub_right, sup_zero, union_add, union_add_inter_subset, union_add_inter_subset_union, union_div, union_div_inter_subset_union, union_mul, union_mul_inter_subset, union_mul_inter_subset_union, union_sub, union_sub_inter_subset_union, univ_add_of_zero_mem, univ_add_univ, univ_div_univ, univ_mul_of_one_mem, univ_mul_univ, univ_pow, univ_sub_univ, zero_mem_neg_add_iff, zero_mem_nsmul, zero_mem_sub_iff, zero_mem_zero, zero_nonempty, zero_notMem_neg_add_iff, zero_notMem_sub_iff, zero_product_zero, zero_subset, zpow_eq_empty, zsmul_empty, zsmul_eq_empty, zsmul_singleton, piFinset_add, piFinset_div, piFinset_inv, piFinset_mul, piFinset_neg, piFinset_sub, finset, finset, toFinset_add, toFinset_mul, toFinset_one, toFinset_zero, toFinset_add, toFinset_mul, toFinset_one, toFinset_zero | 443 |
| Total | 485 |
| Name | Category | Theorems |
|---|
add 📖 | CompOp | 126 mathmath: MvPolynomial.support_mul, add_empty, addEnergy_eq_sum_sq', addETransformRight.fst_add_snd_subset, card_mul_cast_addConst, instAddLeftMono, sup_add_le, subset_add_right, ruzsa_triangle_inequality_add_sub_add, ruzsa_triangle_inequality_sub_add_sub, card_dvd_card_add_right, add_union, card_le_card_add_self', card_le_card_add_left_of_injective, add_mul_subset, add_singleton, addConvolution_eq_zero, Set.Finite.toFinset_add, Nonempty.add, addDysonETransform.subset, card_mul_addConst, add_eq_empty, card_add_le, small_alternating_nsmul_of_small_tripling, le_inf_add, subset_add, Fintype.piFinset_add, card_le_card_add_self, zero_mem_neg_add_iff, pluennecke_ruzsa_inequality_nsmul_add, univ_add_of_zero_mem, Iic_add_Iic_subset, add_univ_of_zero_mem, op_vadd_finset_subset_add, subset_add_left, card_sub_add_le_card_sub_add_card_add, ruzsa_triangle_inequality_add_add_negAdd, cauchy_davenport_of_isAddTorsionFree, Ici_add_Ioi_subset, card_le_card_add_left, card_le_card_add_right, Nontrivial.add_left, add_inter_subset, add_subset_iff_right, map_op_add, add_subset_iff, union_add, Nontrivial.add_right, add_subset_add, ruzsa_triangle_inequality_negAdd_negAdd_negAdd, Ico_add_Icc_subset, addETransformLeft.fst_add_snd_subset, biUnion_op_vadd_finset, singleton_add_inter, addConvolution_ne_zero, op_vadd_finset_add_eq_add_vadd_finset, inf_add_left, add_subset_iff_left, add_nonempty, Set.toFinset_add, singleton_add, add_eq_zero_iff, image_add_product, singleton_add_singleton, AddMonoidAlgebra.support_mul, ruzsa_triangle_inequality_add_sub_sub, inf_add_right, addConst_mul_card, le_card_add_mul_addEnergy, singletonAddHom_apply, mul_add_subset, addConvolution_pos, imageAddHom_apply, card_add_singleton, inter_add_singleton, Ico_add_Ioc_subset, vadd_finset_subset_add, card_add_iff, Iio_add_Iic_subset, Iic_add_Iio_subset, Ioi_add_Ici_subset, empty_add, cast_addConst_mul_card, cauchy_davenport_minOrder_add, card_singleton_add, Ici_add_Ici_subset, mem_add, univ_add_univ, union_add_inter_subset, Icc_add_Icc_subset, image_op_add, add_mem_add, Ioc_add_Ico_subset, instAddRightMono, ruzsa_triangle_inequality_add_addNeg_add, coe_singletonAddHom, Icc_add_Ico_subset, sup_add_right, union_add_inter_subset_union, image_add, coe_add, add_subset_add_left, inter_add_union_subset_union, ruzsa_triangle_inequality_addNeg_addNeg_addNeg, IsApproximateAddSubgroup.card_add_self_le, pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add, imageAddMonoidHom_apply, add_def, card_le_card_add_right_of_injective, coe_list_sum, product_add_product_comm, zero_notMem_neg_add_iff, inter_add_subset, ZMod.cauchy_davenport, card_dvd_card_add_left, sup_add_left, cauchy_davenport_add_of_linearOrder_isCancelAdd, cast_addConst, ruzsa_triangle_inequality_add_add_add, add_subset_add_right, ruzsa_triangle_inequality_negAdd_add_add, ruzsa_triangle_inequality_addNeg_add_add, Nontrivial.add, inter_add_union_subset, mem_sum_list_ofFn, ruzsa_triangle_inequality_sub_add_add
|
addCommMonoid 📖 | CompOp | 1 mathmath: coe_sum
|
addCommSemigroup 📖 | CompOp | — |
addMonoid 📖 | CompOp | 15 mathmath: isAddUnit_iff, image_nsmul_of_ne_zero, nsmul_right_monotone, IsApproximateAddSubgroup.card_nsmul_le, product_nsmul, nsmul_right_strictMono, image_nsmul, le_card_quotient_add_sq_inter_addSubgroup, Nontrivial.nsmul, isAddUnit_coe, isAddUnit_singleton, Nonempty.nsmul, IsAddUnit.finset, card_nsmul_le, nsmul_right_strictMonoOn
|
addSemigroup 📖 | CompOp | — |
addZeroClass 📖 | CompOp | 5 mathmath: singletonAddMonoidHom_apply, coe_coeAddMonoidHom, coe_singletonAddMonoidHom, coeAddMonoidHom_apply, imageAddMonoidHom_apply
|
coeAddMonoidHom 📖 | CompOp | 2 mathmath: coe_coeAddMonoidHom, coeAddMonoidHom_apply
|
coeMonoidHom 📖 | CompOp | 2 mathmath: coeMonoidHom_apply, coe_coeMonoidHom
|
commMonoid 📖 | CompOp | 3 mathmath: coe_prod, nat_divisors_prod, Multiset.nat_divisors_prod
|
commSemigroup 📖 | CompOp | — |
div 📖 | CompOp | 61 mathmath: div_subset_div, le_inf_div, card_mul_divConst, one_mem_div_iff, divConst_mul_card, div_zero_subset, image_div_product, sup_div_right, ruzsa_covering_mul, ruzsa_triangle_inequality_mul_div_mul, sup_div_le, div_nonempty, subset_div_left, subset_div, div_def, ruzsa_triangle_inequality_mul_div_div, ruzsa_triangle_inequality_div_mul_mul, union_div, pluennecke_ruzsa_inequality_pow_div_pow_mul, card_div_mul_le_card_div_mul_card_mul, Nonempty.zero_div, pluennecke_ruzsa_inequality_pow_div, card_le_card_div_self, zero_div_subset, mem_div, div_subset_iff, inter_div_union_subset_union, div_subset_div_left, div_singleton, card_div_le, Fintype.piFinset_div, div_empty, coe_div, div_eq_empty, ruzsa_triangle_inequality_div_mul_div, cast_divConst_mul_card, div_subset_div_right, one_notMem_div_iff, cast_divConst, div_mem_div, div_inter_subset, pluennecke_ruzsa_inequality_pow_div_pow_div, empty_div, Nonempty.one_mem_div, card_le_card_div_right, sup_div_left, inf_div_left, card_le_card_div_left, inf_div_right, ruzsa_triangle_inequality_div_div_div, Nonempty.div_zero, inv_subset_div_right, div_union, image_div, inter_div_subset, singleton_div_singleton, card_mul_cast_divConst, univ_div_univ, union_div_inter_subset_union, singleton_div, Nonempty.div
|
divisionCommMonoid 📖 | CompOp | — |
divisionMonoid 📖 | CompOp | — |
imageAddHom 📖 | CompOp | 2 mathmath: imageAddHom_apply, imageAddMonoidHom_apply
|
imageAddMonoidHom 📖 | CompOp | 1 mathmath: imageAddMonoidHom_apply
|
imageMonoidHom 📖 | CompOp | 1 mathmath: imageMonoidHom_apply
|
imageMulHom 📖 | CompOp | 2 mathmath: imageMonoidHom_apply, imageMulHom_apply
|
imageOneHom 📖 | CompOp | 1 mathmath: imageOneHom_apply
|
imageZeroHom 📖 | CompOp | 1 mathmath: imageZeroHom_apply
|
inv 📖 | CompOp | 61 mathmath: mul_inv_eq_inv_mul_of_doubling_lt_two, card_inv, image_op_inv, ruzsa_triangle_inequality_invMul_mul_mul, inv_smul_finset_distrib, map_op_inv, inv_op_smul_finset_distrib, expect_inv_index, ruzsa_triangle_inequality_mul_mul_invMul, smul_inv_mul_eq_inv_mul_opSMul, inv_mem_inv, inv_singleton, card_inv_le, card_mul_inv_eq_convolution_inv, Equidecomp.IsDecompOn.of_leftInvOn, one_mem_inv_mul_iff, ruzsa_triangle_inequality_invMul_invMul_invMul, inf_inv, mulConst_inv_left, invMulSubgroup_eq_mul_inv, inv_zero, inv_filter_univ, inv_product, inv_smul_finset_distrib₀, convolution_inv, card_smul_inter, dens_inv, image_inv_eq_inv, inv_subset_inv, inv_insert, Nonempty.inv, ruzsa_triangle_inequality_mulInv_mul_mul, mem_inv', card_inv_mul_of_doubling_lt_three_halves, inv_op_smul_finset_distrib₀, ruzsa_triangle_inequality_mulInv_mulInv_mulInv, inv_inter, inv_univ, prod_inv_index, Fintype.piFinset_inv, card_inter_smul, preimage_inv, divConst_inv_right, mulConst_inv_right, ruzsa_triangle_inequality_mul_mulInv_mul, image_inv, one_notMem_inv_mul_iff, coe_inv, mem_inv, invMulSubgroup_eq_inv_mul, card_smul_inter_smul, sup_inv, inv_nonempty_iff, inv_eq_empty, divConst_inv_left, inv_def, inv_subset_div_right, inv_filter, sum_inv_index, inv_empty, smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves
|
monoid 📖 | CompOp | 16 mathmath: isUnit_coe, product_pow, card_pow_le, pow_right_monotone, pow_right_strictMonoOn, Nonempty.pow, image_pow_of_ne_zero, image_pow, IsUnit.finset, le_card_quotient_mul_sq_inter_subgroup, isUnit_iff_singleton, isUnit_singleton, IsApproximateSubgroup.card_pow_le, Nontrivial.pow, isUnit_iff, pow_right_strictMono
|
mul 📖 | CompOp | 138 mathmath: mul_inter_subset, mul_empty, mul_subset_iff_right, empty_mul, mul_subset_mul_left, subset_mul, union_mul, op_smul_finset_mul_eq_mul_smul_finset, ruzsa_triangle_inequality_invMul_mul_mul, mulConst_mul_card, convolution_ne_zero, Nontrivial.mul_right, Equidecomp.IsDecompOn.comp, op_smul_finset_subset_mul, add_mul_subset, imageMonoidHom_apply, small_alternating_pow_of_small_tripling, inf_mul_left, ruzsa_triangle_inequality_mul_div_mul, singleton_mul, ruzsa_triangle_inequality_mul_mul_invMul, Ici_mul_Ioi_subset', mulEnergy_eq_sum_sq', subset_mul_right, Nat.divisors_mul, sup_mul_le, coe_singletonMulHom, coe_mul, List.nat_divisors_prod, card_mul_mulConst, le_card_mul_mul_mulEnergy, image_mul, Ici_mul_Ici_subset', ruzsa_triangle_inequality_mul_div_div, one_mem_inv_mul_iff, ruzsa_triangle_inequality_invMul_invMul_invMul, IsApproximateSubgroup.card_mul_self_le, Iic_mul_Iic_subset', card_le_card_mul_right₀, ruzsa_triangle_inequality_div_mul_mul, singleton_mul_inter, pluennecke_ruzsa_inequality_pow_div_pow_mul, le_inf_mul, univ_mul_univ, instNoZeroDivisors, card_le_card_mul_left_of_injective, card_le_card_mul_self', card_div_mul_le_card_div_mul_card_mul, cast_mulConst_mul_card, card_le_card_mul_self, Ico_mul_Icc_subset', Ioc_mul_Ico_subset', mulDysonETransform.subset, mul_eq_empty, Nonempty.mul_zero, card_mul_iff, image_op_mul, coe_list_prod, Iic_mul_Iio_subset', instMulRightMono, mul_subset_mul_right, ruzsa_triangle_inequality_mulInv_mul_mul, ruzsa_triangle_inequality_mul_mul_mul, mul_subset_iff_left, Fintype.piFinset_mul, SkewMonoidAlgebra.support_mul, singleton_mul_singleton, mul_add_subset, product_mul_product_comm, map_op_mul, Nontrivial.mul, card_mul_le, inf_mul_right, union_mul_inter_subset, Iio_mul_Iic_subset', inter_mul_union_subset, Icc_mul_Ico_subset', inter_mul_union_subset_union, ruzsa_triangle_inequality_mulInv_mulInv_mulInv, mul_univ_of_one_mem, cast_mulConst, card_mul_cast_mulConst, imageMulHom_apply, Icc_mul_Icc_subset', cauchy_davenport_mul_of_linearOrder_isCancelMul, univ_mul_of_one_mem, mul_nonempty, card_dvd_card_mul_left, image_mul_product, card_le_card_mul_right_of_injective, card_le_card_mul_right, instMulLeftMono, convolution_eq_zero, card_le_card_mul_left₀, ruzsa_triangle_inequality_mul_mulInv_mul, mul_subset_iff, ruzsa_triangle_inequality_div_mul_div, one_notMem_inv_mul_iff, mulETransformRight.fst_mul_snd_subset, cauchy_davenport_of_isMulTorsionFree, Set.toFinset_mul, union_mul_inter_subset_union, mul_subset_mul, card_le_card_mul_self₀, singletonMulHom_apply, card_mul_singleton, Nonempty.zero_mul, Nonempty.mul, pluennecke_ruzsa_inequality_pow_mul, Nontrivial.mul_left, Set.Finite.toFinset_mul, card_le_card_mul_left, mul_def, sup_mul_left, Equidecomp.IsDecompOn.comp', biUnion_op_smul_finset, convolution_pos, cauchy_davenport_minOrder_mul, subset_mul_left, inter_mul_singleton, Ico_mul_Ioc_subset', zero_mul_subset, mul_eq_one_iff, mul_zero_subset, MonoidAlgebra.support_mul, mul_union, card_singleton_mul, mul_singleton, sup_mul_right, Subgroup.closure_mul_image_eq_top', mul_mem_mul, Ioi_mul_Ici_subset', inter_mul_subset, mulETransformLeft.fst_mul_snd_subset, mem_prod_list_ofFn, card_dvd_card_mul_right, smul_finset_subset_mul, mem_mul
|
mulOneClass 📖 | CompOp | 6 mathmath: Nat.divisorsHom_apply, coeMonoidHom_apply, imageMonoidHom_apply, singletonMonoidHom_apply, coe_coeMonoidHom, coe_singletonMonoidHom
|
neg 📖 | CompOp | 55 mathmath: image_neg, neg_insert, neg_op_vadd_finset_distrib, neg_filter_univ, addConst_neg_right, neg_filter, neg_inter, zero_mem_neg_add_iff, Fintype.piFinset_neg, prod_neg_index, neg_singleton, subConst_neg_left, ruzsa_triangle_inequality_add_add_negAdd, subConst_neg_right, neg_subset_neg, smul_neg, ruzsa_triangle_inequality_negAdd_negAdd_negAdd, card_inter_vadd, map_op_neg, neg_product, smul_finset_neg, coe_neg, neg_def, neg_empty, preimage_neg, dens_neg, card_neg, addConst_neg_left, neg_smul_finset, expect_neg_index, neg_subset_sub_right, sup_neg, image_neg_eq_neg, Nonempty.neg, neg_mem_neg, addConvolution_neg, neg_eq_empty, ruzsa_triangle_inequality_add_addNeg_add, mem_neg, card_vadd_inter, ruzsa_triangle_inequality_addNeg_addNeg_addNeg, inf_neg, neg_nonempty_iff, mem_neg', neg_univ, neg_smul, zero_notMem_neg_add_iff, card_add_neg_eq_addConvolution_neg, card_vadd_inter_vadd, card_neg_le, ruzsa_triangle_inequality_negAdd_add_add, ruzsa_triangle_inequality_addNeg_add_add, image_op_neg, neg_vadd_finset_distrib, sum_neg_index
|
npow 📖 | CompOp | 30 mathmath: mem_pow, singleton_pow, product_pow, pow_subset_pow_right, pow_subset_pow, image_pow_of_ne_zero, pow_mem_pow, image_pow, pow_subset_pow_mul_of_sq_subset_mul, pluennecke_ruzsa_inequality_pow_div_pow_mul, pluennecke_ruzsa_inequality_pow_div, one_mem_pow, Nonempty.card_pow_mono, empty_pow, pow_eq_empty, inter_pow_subset, card_pow_mono, card_le_card_pow, card_pow_quotient_mul_pow_inter_subgroup_le, pow_subset_pow_left, pluennecke_ruzsa_inequality_pow_div_pow_div, small_pow_of_small_tripling, image_op_pow, pluennecke_ruzsa_inequality_pow_mul, pow_ssubset_pow_succ_of_pow_ne_closure, subset_pow, add_one_le_card_pow, coe_pow, map_op_pow, univ_pow
|
nsmul 📖 | CompOp | 30 mathmath: nsmul_subset_nsmul, subset_nsmul, nsmul_mem_nsmul, nsmul_empty, nsmul_eq_empty, pluennecke_ruzsa_inequality_nsmul_add, map_op_nsmul, image_nsmul_of_ne_zero, add_nonneg_card_nsmul, nsmul_subset_nsmul_left, zero_mem_nsmul, Nonempty.card_nsmul_mono, card_nsmul_quotient_add_nsmul_inter_addSubgroup_le, mem_nsmul, product_nsmul, nsmul_subset_nsmul_right, image_nsmul, pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub, coe_nsmul, inter_nsmul_subset, nsmul_singleton, card_le_card_nsmul, nsmul_univ, pluennecke_ruzsa_inequality_nsmul_sub, pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add, small_nsmul_of_small_tripling, card_nsmul_mono, image_op_nsmul, nsmul_ssubset_nsmul_succ_of_nsmul_ne_closure, nsmul_subset_nsmul_add_of_sq_subset_add
|
one 📖 | CompOp | 41 mathmath: sup_one, Nonempty.subset_one_iff, map_op_one, coe_one, MonoidAlgebra.support_one_subset, preimage_mul_left_one, max'_one, one_mem_one, SkewMonoidAlgebra.support_one, SkewMonoidAlgebra.support_one_subset, small_alternating_pow_of_small_tripling, card_one, preimage_mul_right_one', image_op_one, one_subset, map_one, min_one, inf'_one, coe_singletonOneHom, List.nat_divisors_prod, mem_one, preimage_mul_right_one, one_nonempty, subset_one_iff_eq, coe_list_prod, coe_eq_one, min'_one, preimage_mul_left_one', Set.toFinset_one, imageOneHom_apply, sup'_one, singletonOneHom_apply, inf_one, image_one, one_product_one, singleton_one, mul_eq_one_iff, MonoidAlgebra.support_one, max_one, Set.Finite.toFinset_one, mem_prod_list_ofFn
|
semigroup 📖 | CompOp | — |
singletonAddHom 📖 | CompOp | 2 mathmath: singletonAddHom_apply, coe_singletonAddHom
|
singletonAddMonoidHom 📖 | CompOp | 2 mathmath: singletonAddMonoidHom_apply, coe_singletonAddMonoidHom
|
singletonMonoidHom 📖 | CompOp | 2 mathmath: singletonMonoidHom_apply, coe_singletonMonoidHom
|
singletonMulHom 📖 | CompOp | 2 mathmath: coe_singletonMulHom, singletonMulHom_apply
|
singletonOneHom 📖 | CompOp | 2 mathmath: coe_singletonOneHom, singletonOneHom_apply
|
singletonZeroHom 📖 | CompOp | 2 mathmath: singletonZeroHom_apply, coe_singletonZeroHom
|
sub 📖 | CompOp | 56 mathmath: Nonempty.zero_mem_sub, zero_mem_sub_iff, singleton_sub, inter_sub_union_subset_union, card_mul_subConst, ruzsa_triangle_inequality_add_sub_add, ruzsa_triangle_inequality_sub_add_sub, Nonempty.sub, inf_sub_left, ruzsa_covering_add, coe_sub, inter_sub_subset, cast_subConst_mul_card, mem_sub, card_le_card_sub_right, union_sub, card_sub_add_le_card_sub_add_card_add, sub_subset_sub, inf_sub_right, card_mul_cast_subConst, sup_sub_right, sub_mem_sub, image_sub_product, sup_sub_le, singleton_sub_singleton, sub_eq_empty, Fintype.piFinset_sub, sub_singleton, zero_notMem_sub_iff, sup_sub_left, ruzsa_triangle_inequality_add_sub_sub, pluennecke_ruzsa_inequality_nsmul_sub_nsmul_sub, sub_nonempty, cast_subConst, sub_inter_subset, sub_def, sub_subset_sub_right, subset_sub_left, subConst_mul_card, subset_sub, neg_subset_sub_right, univ_sub_univ, sub_subset_iff, card_le_card_sub_self, card_le_card_sub_left, ruzsa_triangle_inequality_sub_sub_sub, sub_subset_sub_left, card_sub_le, sub_union, union_sub_inter_subset_union, pluennecke_ruzsa_inequality_nsmul_sub, sub_empty, pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add, le_inf_sub, empty_sub, ruzsa_triangle_inequality_sub_add_add
|
subtractionCommMonoid 📖 | CompOp | — |
subtractionMonoid 📖 | CompOp | — |
zero 📖 | CompOp | 73 mathmath: Finsupp.rangeSingleton_support, map_zero, min_zero, Nonempty.zero_smul, zero_nonempty, inf'_zero, div_zero_subset, mem_zero, inf_zero, small_alternating_nsmul_of_small_tripling, preimage_add_left_zero, Finsupp.mem_rangeSingleton_apply_iff, zero_product_zero, DFinsupp.mem_singleton_apply_iff, Set.toFinset_zero, Finsupp.rangeIcc_toFun, image_zero, coe_eq_zero, max'_zero, Finsupp.rangeIcc_apply, DFinsupp.support_rangeIcc_subset, card_zero, inv_zero, instNoZeroDivisors, Nonempty.zero_div, map_op_zero, DFinsupp.Icc_eq, zero_subset, sup_zero, Behrend.sphere_zero_subset, image_op_zero, max_zero, min'_zero, Nonempty.mul_zero, add_eq_zero_iff, zero_div_subset, singleton_zero, Finsupp.mem_rangeIcc_apply_iff, AddMonoidAlgebra.support_one_subset, sup'_zero, Finsupp.card_pi, zero_mem_zero, DFinsupp.card_pi, DFinsupp.mem_pi, Finsupp.rangeSingleton_apply, coe_zero, Finsupp.coe_rangeIcc, DFinsupp.rangeIcc_apply, subset_zero_iff_eq, DFinsupp.mem_rangeIcc_apply_iff, zero_smul_finset, Nonempty.subset_zero_iff, Finsupp.Icc_eq, Finsupp.rangeIcc_support, Nonempty.zero_mul, preimage_add_left_zero', preimage_add_right_zero, zero_smul_finset_subset, singletonZeroHom_apply, zero_smul_subset, Nonempty.div_zero, zero_mul_subset, coe_list_sum, smul_zero_subset, Nonempty.smul_zero, mul_zero_subset, preimage_add_right_zero', Set.Finite.toFinset_zero, coe_singletonZeroHom, Finsupp.mem_pi, AddMonoidAlgebra.support_one, imageZeroHom_apply, mem_sum_list_ofFn
|
zpow 📖 | CompOp | 6 mathmath: singleton_zpow, small_alternating_pow_of_small_tripling, empty_zpow, zpow_eq_empty, Nonempty.zpow, coe_zpow
|
zsmul 📖 | CompOp | 6 mathmath: small_alternating_nsmul_of_small_tripling, Nonempty.zsmul, zsmul_eq_empty, zsmul_singleton, zsmul_empty, coe_zsmul
|