| Metric | Count |
|---|
Definitionspointwise_nat_action, NPow, NSMul, ZSMul, add, addCommMonoid, addCommSemigroup, addMonoid, addSemigroup, addZeroClass, commMonoid, commSemigroup, div, divisionCommMonoid, divisionMonoid, inv, involutiveInv, involutiveNeg, monoid, mul, mulOneClass, neg, one, semigroup, singletonAddHom, singletonAddMonoidHom, singletonMonoidHom, singletonMulHom, singletonOneHom, singletonZeroHom, sub, subtractionCommMonoid, subtractionMonoid, zero | 34 |
Theoremsone_notMem_div_set, zero_notMem_sub_set, add, div, inv, mul, neg, sub, add, div, inv, mul, neg, nsmul, of_add_left, of_add_right, of_div_left, of_div_right, of_mul_left, of_mul_right, 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_empty, add_eq_empty, add_eq_zero_iff, add_image_prod, add_inter_subset, add_mem_add, add_nonempty, add_singleton, add_subset_add, add_subset_add_left, add_subset_add_right, add_subset_iff, add_subset_range, add_union, add_univ, add_univ_of_zero_mem, coe_singletonAddHom, coe_singletonAddMonoidHom, coe_singletonMonoidHom, coe_singletonMulHom, coe_singletonOneHom, coe_singletonZeroHom, compl_inv, compl_neg, 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_subset_range, div_union, empty_add, empty_div, empty_mul, empty_pow, empty_sub, empty_zpow, exists_inv_mem, exists_neg_mem, forall_inv_mem, forall_neg_mem, image2_add, image2_div, image2_mul, image2_sub, image_add, image_add_left, image_add_left', image_add_right, image_add_right', image_div, image_div_prod, image_inv, image_inv_eq_inv, image_inv_of_apply_inv_eq, image_inv_of_apply_inv_eq_inv, image_mul, image_mul_left, image_mul_left', image_mul_prod, image_mul_right, image_mul_right', image_neg, image_neg_eq_neg, image_neg_of_apply_neg_eq, image_neg_of_apply_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_one, image_op_zero, image_pow, image_pow_of_ne_zero, image_sub, image_zero, instAddLeftMono, instAddRightMono, instMulLeftMono, instMulRightMono, inter_add_subset, inter_add_union_subset, inter_add_union_subset_union, inter_div_subset, inter_div_union_subset_union, inter_inv, inter_mul_subset, inter_mul_union_subset, inter_mul_union_subset_union, inter_neg, inter_nsmul_subset, inter_pow_subset, inter_sub_subset, inter_sub_union_subset_union, inv_empty, inv_eq_empty, inv_insert, inv_mem_inv, inv_pi, inv_preimage, inv_prod, inv_range, inv_setOf, inv_singleton, inv_subset, inv_subset_div_right, inv_subset_inv, inv_univ, isAddUnit_iff, isAddUnit_iff_singleton, isAddUnit_singleton, isUnit_iff, isUnit_iff_singleton, isUnit_singleton, mem_add, mem_div, mem_inv, mem_mul, mem_neg, mem_one, mem_sub, mem_zero, mul_empty, mul_eq_empty, mul_eq_one_iff, mul_inter_subset, mul_mem_mul, mul_nonempty, mul_singleton, mul_subset_iff, mul_subset_mul, mul_subset_mul_left, mul_subset_mul_right, mul_subset_range, mul_union, mul_univ, mul_univ_of_one_mem, neg_empty, neg_eq_empty, neg_insert, neg_mem_neg, neg_pi, neg_preimage, neg_prod, neg_range, neg_setOf, neg_singleton, neg_subset, neg_subset_neg, neg_subset_sub_right, neg_univ, nonempty_image_addLeft_neg_inter_iff, nonempty_image_addRight_neg_inter_iff, nonempty_image_mulLeft_inv_inter_iff, nonempty_image_mulRight_inv_inter_iff, nonempty_inv, nonempty_neg, nsmul_empty, nsmul_eq_empty, nsmul_mem_nsmul, nsmul_prod, 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_prod_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, preimage_add_left_singleton, preimage_add_left_zero, preimage_add_left_zero', preimage_add_preimage_subset, preimage_add_right_singleton, preimage_add_right_zero, preimage_add_right_zero', preimage_div, preimage_div_preimage_subset, preimage_mul, preimage_mul_left_one, preimage_mul_left_one', preimage_mul_left_singleton, preimage_mul_preimage_subset, preimage_mul_right_one, preimage_mul_right_one', preimage_mul_right_singleton, preimage_nsmul_subset, preimage_pow_subset, preimage_sub, preimage_sub_preimage_subset, prod_add_prod_comm, prod_mul_prod_comm, prod_pow, singletonAddHom_apply, singletonAddMonoidHom_apply, singletonMonoidHom_apply, singletonMulHom_apply, singleton_add, singleton_add_singleton, singleton_div, singleton_div_singleton, singleton_mul, singleton_mul_singleton, singleton_one, singleton_pow, singleton_sub, singleton_sub_singleton, singleton_zero, singleton_zpow, sub_empty, sub_eq_empty, sub_image_prod, sub_inter_subset, sub_mem_sub, sub_nonempty, sub_singleton, sub_subset_iff, sub_subset_range, sub_subset_sub, sub_subset_sub_left, sub_subset_sub_right, sub_union, subset_add_left, subset_add_right, subset_div_left, subset_mul_left, subset_mul_right, subset_nsmul, subset_one_iff_eq, subset_pow, subset_sub_left, subset_zero_iff_eq, union_add, union_add_inter_subset, union_add_inter_subset_union, union_div, union_div_inter_subset_union, union_inv, union_mul, union_mul_inter_subset, union_mul_inter_subset_union, union_neg, union_sub, union_sub_inter_subset_union, univ_add, univ_add_of_zero_mem, univ_add_univ, univ_div_univ, univ_mul, 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_prod_zero, zero_subset, zpow_eq_empty, zsmul_empty, zsmul_eq_empty, zsmul_singleton | 328 |
| Total | 362 |
| Name | Category | Theorems |
|---|
NPow 📖 | CompOp | 41 mathmath: empty_pow, Ici_pow_eq, Submonoid.closure_pow, pow_mem_pow, image_pow_of_ne_zero, Submodule.span_pow, SubMulAction.subset_coe_pow, LinearEquiv.dilatransvections_pow_mono, singleton_pow, Finset.pow_right_strictMonoOn, pow_eq_empty, pow_subset_pow_mul_of_sq_subset_mul, one_mem_pow, mem_pow_iff_prod, preimage_pow_subset, IsApproximateSubgroup.pow_inter_pow, inter_pow_subset, Multiplicative.toAdd_image_nsmul, pow_subset_pow_right, AddSubmonoid.pow_eq_closure_pow_set, LinearEquiv.transvections_pow_mono, pow_subset_pow_left, Filter.pow_mem_pow, prod_pow, AddSubmonoid.pow_subset_pow, subset_pow, AddSubmonoid.closure_pow, Submodule.pow_eq_span_pow_set, Group.card_pow_eq_card_pow_card_univ, Submodule.pow_subset_pow, pow_subset_pow, mem_pow, IsApproximateSubgroup.pow_inter_pow_covBySMul_sq_inter_sq, univ_pow, coe_powCardSubgroup, Subgroup.closure_pow, Finset.coe_pow, image_pow, Multiplicative.ofAdd_image_nsmul, SubMulAction.coe_pow, Finsupp.image_pow_eq_finsuppProd_image
|
NSMul 📖 | CompOp | 35 mathmath: nsmul_empty, Ici_nsmul_eq, AddSubgroup.closure_nsmul, AddSubmonoid.closure_nsmul, zero_mem_nsmul, mem_nsmul_iff_sum, nsmul_subset_nsmul_right, IsApproximateAddSubgroup.nsmul_inter_nsmul, inter_nsmul_subset, coe_smulCardAddSubgroup, image_nsmul_of_ne_zero, AddGroup.card_nsmul_eq_card_nsmul_card_univ, IsApproximateAddSubgroup.two_nsmul_covByVAdd, Multiplicative.toAdd_image_nsmul, preimage_nsmul_subset, Filter.nsmul_mem_nsmul, nsmul_singleton, mem_nsmul, MvPolynomial.restrictSupport_nsmul, Finset.coe_nsmul, nsmul_subset_nsmul_add_of_sq_subset_add, subset_nsmul, Finsupp.degree_preimage_nsmul, nsmul_univ, image_nsmul, nsmul_subset_nsmul_left, nsmul_eq_empty, nsmul_prod, IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sq, nsmul_subset_nsmul, nsmul_mem_nsmul, ConvexBody.coe_nsmul, Finsupp.nsmul_single_one_image, Multiplicative.ofAdd_image_nsmul, Finset.nsmul_right_strictMonoOn
|
ZSMul 📖 | CompOp | 5 mathmath: zsmul_singleton, Nonempty.zsmul, zsmul_eq_empty, Finset.coe_zsmul, zsmul_empty
|
add 📖 | CompOp | 300 mathmath: Filter.HasBasis.add_self, mem_list_sum, IsPathConnected.add, Ioi_add_Ici_subset, HasCompactSupport.convolution_integrand_bound_left, HasFPowerSeriesWithinAt.comp_sub, Nontrivial.add, AddSubmonoid.add_subset_closure, subset_interior_add', compact_open_separated_add_right, Bornology.isVonNBounded_add_of_nonempty, mem_sum_list_ofFn, add_iInter₂_subset, MeasureTheory.Measure.eventually_nonempty_inter_smul_of_density_one, Bornology.isVonNBounded_add_self, add_subset_add_left, IsAddFreimanHom.add, Multiplicative.toAdd_image_setMul, AnalyticOn.comp_sub, IsLowerSet.add_right, UpperSet.coe_add, Filter.HasBasis.add, Ici_add_Ici_subset, AddSubgroup.normal_add, IsUpperSet.add_right, list_sum_singleton, Ico_add_Icc_subset, egauge_add_add_le, Iio_add_Iic_subset, Submodule.coe_sup, AddSubgroup.add_normal, Convex.set_combo_subset, IsOpen.add_closure, exists_closed_nhds_zero_neg_eq_add_subset, MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero, op_vadd_set_add_eq_add_vadd_set, Multiplicative.ofAdd_image_setAdd, iUnion_add_right_image, Finite.toFinset_add, closedBall_add_closedBall, AddGroupFilterBasis.add', IsCompact.closedBall_zero_add, union_add, add_iInter_subset, add_upperClosure, Icc_add_Icc_subset, infinite_add, op_vadd_set_subset_add, instAddLeftMono, BddAbove.add, subset_interior_add_left, Convex.combo_interior_closure_subset_interior, prod_add_prod_comm, MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux1, star_add, JoinedIn.add, natCard_add_le, convexHull_add, Iic_add_Iic_subset, IsTopologicalAddGroup.exists_antitone_basis_nhds_zero, AddSemigroupIdeal.coe_closure, ball_add_ball, AddAction.stabilizer_add_self, singleton_add_singleton, closedBall_add_ball, Balanced.add, add_mul_subset, AddSubgroup.IsComplement.add_eq, Convex.combo_self_interior_subset_interior, list_sum_subset_list_sum, subset_interior_add, add_subset_iff_left, LinearOrderedField.cutMap_add, ball_zero_add_singleton, IsOpen.add_right, BddBelow.add, AddSubmonoid.coe_add_self_eq, Filter.le_add_iff, ball_add_zero, iUnion_add, image_op_vadd, subset_add_left, IsClosed.add_left_of_isCompact, add_subset_range, AddSubgroup.card_add_eq_card_addSubgroup_add_card_quotient, starConvex_iff_pointwise_add_subset, AddSubgroup.coe_add_of_left_le_normalizer_right, add_inter_subset, subset_add_right, convex_list_sum, add_subset_iff, ball_add_closedBall, Icc_add_Icc, AnalyticOnNhd.comp_sub, univ_add_of_zero_mem, eventually_singleton_add_smul_subset, add_ball_zero, AddSubmonoid.top_closure_add_self_subset, add_eq_empty, IsOpen.closure_add, convexHull_add_subset, Convex.combo_interior_self_subset_interior, MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux2, add_univ, AddSemigroupIdeal.coe_closure', AddSubgroup.closure_add_le, AddSubgroup.inf_add_assoc, Finite.add, iInter_add_subset, coe_singletonAddHom, Seminorm.ball_add_ball_subset, Nontrivial.add_right, absConvexHull_add_subset, add_mem_add, QuotientAddGroup.image_coe_inj, iUnion_op_vadd_set, preimage_add_preimage_subset, balancedHull_add_subset, inter_add_union_subset_union, AddSubgroup.coe_add_of_right_le_normalizer_left, QuotientAddGroup.preimage_image_mk_eq_add, Finsupp.degree_preimage_add, IsWF.add, Convex.add, union_add_inter_subset, add_pair, IsOpen.add_closure_zero_eq, IsTopologicalAddGroup.addNegClosureNhd.add, nsmul_add_addSubgroupClosure, Convex.combo_closure_interior_subset_interior, MeasurableSet.add_closure_zero_eq, Convex.add_smul, Absorbs.add, MapsTo.add, lowerClosure_add, exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add, IsUpperSet.add_left, toFinset_add, add_sUnion, spectrum.add_singleton_eq, iUnion₂_add, inter_add_union_subset, singleton_add_mem_nhds_of_nhds_zero, zero_mem_neg_add_iff, Filter.add_mem_add, MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one, add_image_prod, QuotientAddGroup.dense_image_mk, add_iUnion, StrictConvex.add, spectrum.singleton_add_eq, HasFPowerSeriesWithinOnBall.comp_sub, AnalyticWithinAt.comp_sub, AddSubmonoid.coe_sup, vadd_set_subset_add, singleton_add_closedBall_zero, HomogeneousIdeal.coe_sup, add_lowerClosure, preimage_add, add_nonempty, AddSubmonoid.top_closure_add_self_eq, MeasureTheory.measure_add_closure_zero, Iic_add_Iio_subset, IsOpen.add_left, IsCompact.add_closure_zero_eq_closure, closedBall_add_singleton, Archimedean.ratLt_add, IsTopologicalAddGroup.exist_add_closure_nhds, finite_add, QuotientAddGroup.preimage_image_coe, AddSubmonoid.closure_add_le, add_empty, ball_add, singleton_add, add_subset_add, upperClosure_add_distrib, singletonAddHom_apply, add_singleton, IsWF.min_add, add_ball, HahnSeries.support_mul_subset_add_support, isBounded_add, Bornology.isVonNBounded_add, ball_add_singleton, AddSubmonoid.sup_eq_closure_add, subset_add_closure_zero, Finset.support_addAntidiagonal_subset_add, addSubgroupClosure_add, vectorSpan_add_self, Bornology.IsVonNBounded.add, exists_open_nhds_zero_add_subset, ConvexCone.coe_add, Nontrivial.add_left, univ_add, ContinuousMap.adjoin_id_eq_span_one_add, MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_smul, AddSubgroup.add_inf_assoc, IsLUB.add, coe_add_coe, sUnion_add, IsSemilinearSet.add, MvPolynomial.restrictSupport_add, upperClosure_add, sInf_add, convex_iff_pointwise_add_subset, Icc_add_Ico_subset, add_sInter_subset, IsPWO.add, subset_upperBounds_add, union_add_inter_subset_union, AddSubgroup.set_add_normalizer_comm, Nonempty.add, univ_add_univ, LowerSet.coe_add, compl_add_closure_zero_eq_iff, add_eq_zero_iff, AddSubmonoid.add_subset, BddAbove.add, Cardinal.mk_add_le, add_subset_iff_right, Ici_add_Ioi_subset, HahnSeries.support_mul_subset, list_sum_mem_list_sum, sInter_add_subset, image_op_add, csSup_add, SeminormFamily.basisSets_add, Ioc_add_Ico_subset, MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one_aux, add_subset_add_right, Subrepresentation.coe_sup, AddSubsemigroup.top_closure_add_self_subset, sSup_add, Filter.mem_add, zero_notMem_neg_add_iff, add_singleton_mem_nhds_of_nhds_zero, add_mem_lowerBounds_add, AddAction.add_stabilizer_self, MeasureTheory.support_convolution_subset_swap, AddSubgroup.exists_right_transversal_of_le, IsCompact.closedBall_add, ediam_add_le, Finset.coe_add, singleton_add_ball_zero, AddSubgroup.sup_eq_closure_add, subset_lowerBounds_add, add_mem_upperBounds_add, convexHull_list_sum, add_addSubgroupClosure, addSubgroupClosure_add_nsmul, iInter₂_add_subset, IsClosed.add_closure_zero_eq, ConvexBody.coe_add, singleton_add_ball, IsClosed.add_right_of_isCompact, AddSubgroup.exists_left_transversal_of_le, lowerClosure_add_distrib, mem_add, add_smul_subset, Finset.coe_list_sum, IsCompact.add_closedBall_zero, image_list_sum, compact_open_separated_add_left, MeasureTheory.support_convolution_subset, add_univ_of_zero_mem, mul_add_subset, Ici_add_Ici_eq, AddSubgroup.set_add_normal_comm, IsLinearSet.add, csInf_add, Absorbent.vadd_absorbs, small_add, StarConvex.add, singleton_add_closedBall, instAddRightMono, BoundedAdd.isBounded_add, closedBall_zero_add_singleton, empty_add, HasCompactSupport.convolution_integrand_bound_right, image2_add, AddGroupFilterBasis.subset_add_self, image_add, IsCompact.add_closedBall, subset_interior_add_right, Bornology.IsBounded.add, Seminorm.closedBall_add_closedBall_subset, add_iUnion₂, singleton_add_mem_nhds, add_singleton_mem_nhds, IsLowerSet.add_left, Archimedean.ratLt'_add, IsCompact.add, inter_add_subset, iUnion_add_left_image, IsGLB.add, add_union, AddGroupFilterBasis.add, Ico_add_Ioc_subset, IsCompact.closedBall_sub, pair_add
|
addCommMonoid 📖 | CompOp | 19 mathmath: convexHull_multiset_sum, finset_sum_subset_finset_sum, mem_finset_sum, image_finset_sum, multiset_sum_mem_multiset_sum, convexHull_sum, image_multiset_sum, convex_multiset_sum, image_finset_sum_pi, parallelepiped_eq_sum_segment, mem_fintype_sum, convex_sum, multiset_sum_singleton, multiset_sum_subset_multiset_sum, finset_sum_singleton, finset_sum_mem_finset_sum, parallelepiped_eq_convexHull, image_fintype_sum_pi, Finset.coe_sum
|
addCommSemigroup 📖 | CompOp | — |
addMonoid 📖 | CompOp | 19 mathmath: Nontrivial.nsmul, Nonempty.nsmul, image_nsmul_of_ne_zero, isAddUnit_singleton, nsmul_right_monotone, isAddUnit_iff_singleton, AddSubmonoid.closure_nsmul_le, IsAddUnit.set, preimage_nsmul_subset, nsmul_add_addSubgroupClosure, AddSubgroup.closure_nsmul_le, image_nsmul, Finset.isAddUnit_coe, isAddUnit_iff, nsmul_prod, addSubgroupClosure_add_nsmul, IsApproximateAddSubgroup.nsmul_inter_nsmul_covByVAdd_sq_inter_sq, coe_set_nsmul, IsApproximateAddSubgroup.of_small_tripling
|
addSemigroup 📖 | CompOp | — |
addZeroClass 📖 | CompOp | 7 mathmath: coe_convexAddSubmonoid, Finset.coe_coeAddMonoidHom, singletonAddMonoidHom_apply, convexHullAddMonoidHom_apply, Finset.coeAddMonoidHom_apply, coe_singletonAddMonoidHom, mem_convexAddSubmonoid
|
commMonoid 📖 | CompOp | 15 mathmath: multiset_prod_subset_multiset_prod, Finset.coe_prod, finset_prod_singleton, mem_fintype_prod, image_multiset_prod, Submodule.prod_span, image_finset_prod, finset_prod_subset_finset_prod, multiset_prod_singleton, Ideal.prod_span, mem_finset_prod, multiset_prod_mem_multiset_prod, finset_prod_mem_finset_prod, image_fintype_prod_pi, image_finset_prod_pi
|
commSemigroup 📖 | CompOp | — |
div 📖 | CompOp | 105 mathmath: iInter₂_div_subset, IsOpen.div_closure, IsLowerSet.div_left, subset_interior_div, IsOpen.div_left, singleton_div_closedBall, preimage_div_preimage_subset, div_iInter_subset, Nonempty.div, ball_div_one, iUnion_div_left_image, subset_div_left, univ_div_univ, preimage_div, div_singleton, div_empty, Filter.div_mem_div, MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos_ne_top, div_subset_range, UpperSet.coe_div, Cardinal.mk_div_le, csInf_div, div_mem_div, IsCompact.div_closedBall, div_subset_div_right, singleton_div, div_subset_div_left, singleton_div_closedBall_one, MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos, IsOpen.div_right, IsOpen.closure_div, div_ball, subset_interior_div_right, div_eq_empty, div_inter_subset, IsUpperSet.div_right, div_union, mem_div, Nonempty.one_mem_div, inter_div_union_subset_union, image_div_prod, coe_div_coe, div_iInter₂_subset, ball_div, image2_div, inter_div_subset, iUnion_div, Finite.div, singleton_div_ball_one, MulAction.stabilizer_subset_div_right, closedBall_div_singleton, closedBall_one_div_singleton, Bornology.IsBounded.div, iUnion_div_right_image, IsGLB.div, sInter_div_subset, singleton_div_singleton, ball_one_div_singleton, empty_div, div_subset_div, singleton_div_ball, small_div, div_sUnion, sSup_div, ball_div_singleton, Filter.le_div_iff, inv_subset_div_right, div_iUnion₂, IsCompact.closedBall_one_div, IsUpperSet.div_left, div_ball_one, Disjoint.one_notMem_div_set, one_notMem_div_iff, Nonempty.div_zero, Filter.mem_div, MapsTo.div, union_div, Finset.coe_div, smul_div_smul_comm, infinite_div, LowerSet.coe_div, ruzsa_covering_mul, union_div_inter_subset_union, csSup_div, Filter.HasBasis.div, subset_interior_div_left, one_mem_div_iff, finite_div, div_subset_iff, image_div, Nonempty.zero_div, sUnion_div, natCard_div_le, zero_div_subset, IsMulFreimanHom.div, div_zero_subset, IsCompact.div_closedBall_one, iUnion₂_div, IsLowerSet.div_right, iInter_div_subset, sInf_div, IsLUB.div, div_sInter_subset, div_iUnion, div_nonempty
|
divisionCommMonoid 📖 | CompOp | — |
divisionMonoid 📖 | CompOp | — |
inv 📖 | CompOp | 123 mathmath: iUnion_inv, inv_eq_empty, Nonempty.inv, infEdist_inv, Submonoid.coe_invOrderIso_apply, MeasureTheory.measure_inv_null, mem_smul_set_inv, JoinedIn.inv, compl_inv, inv_Ico, Submonoid.coe_invOrderIso_symm_apply, inv_Ioc, isGLB_inv', ball_div_one, IsTopologicalGroup.mulInvClosureNhd.inv, ncard_inv, MeasureTheory.eventuallyConst_inv_set_ae, inv_pi, inv_Iio₀, inv_Ioo_0_right, star_inv', Subgroup.closure_toSubmonoid, infinite_inv, bddAbove_inv, exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul, inv_mem_inv, sInter_inv, inv_Ioi, Cardinal.mk_inv, isLUB_inv, inv_empty, IsLUB.inv, inv_mem_nhds_one, IsPathConnected.inv, sSup_inv, image_inv_of_apply_inv_eq, IsDiscrete.exists_nhds_eq_one_of_image_mulRight_inter_nonempty, isGLB_inv, image_inv_of_apply_inv_eq_inv, star_inv, inv_zero, sInf_inv, inv_Ici, inv_coe_set, inv_Icc, Bornology.IsBounded.inv, BddAbove.inv, IsApproximateSubgroup.inv_eq_self, ball_div, inter_inv, exists_closed_nhds_one_inv_eq_mul_subset, inv_prod, isLUB_inv', inv_setOf, infEdist_inv_inv, inv_range, inv_smul_set_distrib₀, union_inv, totallyBounded_inv, Submonoid.coe_inv, nonempty_image_mulLeft_inv_inter_iff, natCard_inv, csSup_inv, bddBelow_inv, inv_Ioi₀, IsCompact.inv, inv_smul_set_distrib, Filter.HasBasis.inv, MeasureTheory.Measure.inv_apply, IsUpperSet.inv, finite_inv, inv_subset_div_right, spectrum.map_inv, inv_Ioo, IsCompact.closedBall_one_div, Finite.inv, IsClosed.inv, one_notMem_inv_mul_iff, inv_uIcc, image_op_inv, Subgroup.inv_subset_closure, BddBelow.inv, Filter.inv_mem_inv, MeasurableSet.inv, inv_op_smul_set_distrib, inv_subset_inv, Subgroup.closure_inv, Finset.coe_inv, nonempty_inv, inv_subset, inv_univ, inv_singleton, IsOpen.inv, Submonoid.mem_closure_inv, inv_insert, IsMulFreimanHom.inv, IsLowerSet.inv, inv_closedBall, inv_cthickening, nonempty_image_mulRight_inv_inter_iff, inv_Iic, Submonoid.closure_inv, inv_ball, inv_Ioo_0_left, inv_preimage, inv_Iio, image_inv_eq_inv, image_inv, inv_thickening, inv_closure, iInter_inv, infEDist_inv_inv, MeasureTheory.Measure.measure_inv, csInf_inv, sUnion_inv, infEDist_inv, MapsTo.inv, IsDiscrete.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty, IsGLB.inv, inv_op_smul_set_distrib₀, encard_inv, one_mem_inv_mul_iff, mem_inv
|
involutiveInv 📖 | CompOp | 3 mathmath: mulDissociated_inv, MulDissociated.inv, MeasureTheory.IntegrableOn.comp_inv
|
involutiveNeg 📖 | CompOp | 10 mathmath: MeasureTheory.IntegrableOn.comp_neg, RingPreordering.coe_support, AddDissociated.neg, addDissociated_neg, SimpleGraph.circulantGraph_eq_symm, RingPreordering.coe_supportAddSubgroup, Submodule.neg_coe, support_conjneg, ConjRootClass.carrier_neg, PointedCone.salient_iff_inter_neg_eq_singleton
|
monoid 📖 | CompOp | 20 mathmath: Finset.isUnit_coe, image_pow_of_ne_zero, Submonoid.closure_pow_le, Nonempty.pow, subgroupClosure_mul_pow, preimage_pow_subset, isUnit_iff, pow_right_monotone, pow_mul_subgroupClosure, IsApproximateSubgroup.of_small_tripling, isUnit_singleton, prod_pow, Nontrivial.pow, IsApproximateSubgroup.sq_covBySMul, coe_set_pow, IsApproximateSubgroup.pow_inter_pow_covBySMul_sq_inter_sq, Subgroup.closure_pow_le, isUnit_iff_singleton, image_pow, IsUnit.set
|
mul 📖 | CompOp | 273 mathmath: IsOpen.mul_left, subset_interior_mul_left, Subgroup.sup_eq_closure_mul, instNoZeroDivisors, mul_ball, QuotientGroup.image_coe_inj, smul_set_subset_mul, iUnion_mul_left_image, exists_open_nhds_one_mul_subset, inter_mul_subset, Nontrivial.mul, TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure, union_mul, Submonoid.top_closure_mul_self_subset, mul_univ, Multiplicative.toAdd_image_setMul, ball_mul_singleton, IsCompact.closedBall_mul, mul_mem_lowerBounds_mul, subset_interior_mul', mul_eq_empty, IsCompact.mul_closedBall_one, MulAction.stabilizer_mul_self, mul_zero_subset, Icc_mul_Icc, Icc_mul_Icc_subset', mul_inter_subset, IsPathConnected.mul, Subgroup.mul_normal, Subsemigroup.top_closure_mul_self_subset, Subgroup.exists_left_transversal_of_le, Subgroup.coe_mul_of_left_le_normalizer_right, Nonempty.mul, instMulRightMono, Multiplicative.ofAdd_image_setAdd, coe_mul_coe, IsOpen.mul_closure_one_eq, Ico_mul_Ioc_subset', Ico_mul_Icc_subset', ball_mul_one, SetSemiring.down_mul, Finite.mul, MulAction.mul_stabilizer_self, singleton_mul_closedBall_one, exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul, IsUpperSet.mul_right, QuotientGroup.preimage_image_mk_eq_mul, mul_iUnion, univ_mul, singleton_mul_mem_nhds, IsTopologicalGroup.exists_antitone_basis_nhds_one, image_mul_prod, pair_mul, Submonoid.sup_eq_closure_mul, Subgroup.set_mul_normalizer_comm, mul_singleton, ball_mul, Submodule.span_mul_span, iInter_mul_subset, AlgebraicGeometry.Scheme.zeroLocus_setMul, mem_prod_list_ofFn, infinite_mul, add_mul_subset, csInf_mul, SemigroupIdeal.coe_closure, subset_upperBounds_mul, Subgroup.set_mul_normal_comm, subgroupClosure_mul_pow, Filter.mul_mem_mul, csSup_mul, prod_mul_prod_comm, preimage_mul_preimage_subset, Finset.coe_mul, univ_mul_univ, Ioc_mul_Ico_subset', iUnion_mul, sSup_mul, Submodule.mem_span_mul_finite_of_mem_mul, upperClosure_mul, Filter.mem_mul, Subgroup.subgroup_mul_singleton, sInf_mul, up_mul, BddAbove.mul, mul_sUnion, JoinedIn.mul, iInter₂_mul_subset, Filter.le_mul_iff, image_list_prod, isBounded_mul, IsCompact.mul_closedBall, mul_eq_one_iff, mul_subset_mul_right, Subgroup.closure_mul_image_eq, mul_iInter₂_subset, Finset.invMulSubgroup_eq_mul_inv, IsLUB.mul, IsCompact.closedBall_one_mul, IsCompact.closedBall_div, Submonoid.mul_subset, Ideal.span_mul_span', Finset.doubling_lt_two, IsClosed.mul_left_of_isCompact, exists_closed_nhds_one_inv_eq_mul_subset, GroupFilterBasis.mul, Submonoid.mul_subset_closure, RingFilterBasis.mul', image_mul, Finset.doubling_lt_golden_ratio, IsClosed.mul_right_of_isCompact, Subgroup.closure_mul_image_mul_eq_top, IsGLB.mul, MapsTo.mul, Subgroup.singleton_mul_subgroup, mul_singleton_mem_nhds, op_smul_set_mul_eq_mul_smul_set, compact_open_separated_mul_left, UpperSet.coe_mul, SubMulAction.coe_mul, IsClosed.mul_closure_one_eq, Ici_mul_Ioi_subset', Ideal.span_mul_span, pow_mul_subgroupClosure, GroupFilterBasis.mul', Subgroup.normal_mul, mul_iUnion₂, BoundedMul.isBounded_mul, ball_one_mul_singleton, small_mul, singleton_mul_mem_nhds_of_nhds_one, IsUpperSet.mul_left, Finset.coe_list_prod, iUnion_mul_right_image, image2_mul, TwoSidedIdeal.set_mul_subset, mul_mem_upperBounds_mul, IsCompact.mul_closure_one_eq_closure, TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_nonunital, singleton_mul_closedBall, GroupFilterBasis.subset_mul_self, TwoSidedIdeal.subset_mul_set, BddAbove.mul, sInter_mul_subset, FractionalIdeal.mem_span_mul_finite_of_mem_mul, singletonMulHom_apply, Submonoid.closure_mul_le, list_prod_singleton, Iic_mul_Iic_subset', RingFilterBasis.mul, mul_subset_iff, iUnion_op_smul_set, Nonempty.zero_mul, coe_singletonMulHom, zero_mul_subset, NonarchimedeanRing.mul_subset, AddSubmonoid.mul_subset_mul, Submonoid.coe_sup, mul_pair, one_notMem_inv_mul_iff, subset_mul_closure_one, Ici_mul_Ici_eq, mul_subset_iff_right, compact_open_separated_mul_right, empty_mul, mul_sInter_subset, mul_singleton_mem_nhds_of_nhds_one, Cardinal.mk_mul_le, Subgroup.closure_mul_le, IsWF.min_mul, Icc_mul_Ico_subset', mul_subset_iff_left, mul_subset_range, MeasurableSet.mul_closure_one_eq, Nontrivial.mul_right, image_op_smul, sUnion_mul, IsMulFreimanHom.mul, Subgroup.exists_right_transversal_of_le, mul_ball_one, Submodule.mul_subset_mul, singleton_mul_ball_one, natCard_mul_le, subset_mul_right, Nontrivial.mul_left, Subgroup.mul_inf_assoc, op_smul_set_subset_mul, mul_nonempty, Finset.card_mul_finset_lt_two, finite_mul, mul_subset_mul_left, mem_list_prod, Subgroup.inf_mul_assoc, Subgroup.closure_mul_image_eq_top, iUnion₂_mul, Finset.invMulSubgroup_eq_inv_mul, closedBall_mul_singleton, mul_subgroupClosure, Iio_mul_Iic_subset', Subgroup.IsComplement.mul_eq, toFinset_mul, Bornology.IsBounded.mul, QuotientGroup.preimage_image_coe, list_prod_mem_list_prod, subset_lowerBounds_mul, Subgroup.coe_mul_of_right_le_normalizer_left, inter_mul_union_subset, ediam_mul_le, univ_mul_of_one_mem, Submodule.mul_eq_span_mul_set, union_mul_inter_subset_union, lowerClosure_mul, mul_empty, upperClosure_mul_distrib, IsLowerSet.mul_left, IsOpen.closure_mul, IsTopologicalGroup.exist_mul_closure_nhds, Nonempty.mul_zero, union_mul_inter_subset, instMulLeftMono, IsOpen.mul_closure, Filter.HasBasis.mul_self, Subgroup.card_mul_eq_card_subgroup_mul_card_quotient, lowerClosure_mul_distrib, Finite.toFinset_mul, Submonoid.top_closure_mul_self_eq, mul_univ_of_one_mem, IsPWO.mul, SemigroupIdeal.coe_closure', mul_upperClosure, compl_mul_closure_one_eq_iff, Iic_mul_Iio_subset', IsWF.mul, mul_lowerClosure, Ici_mul_Ici_subset', IsTopologicalGroup.mulInvClosureNhd.mul, Submodule.mul_def, QuotientGroup.dense_image_mk, IsLowerSet.mul_right, IsOpen.mul_right, preimage_mul, singleton_mul, closedBall_one_mul_singleton, SetSemiring.mul_def, BddBelow.mul, mul_union, mul_add_subset, SubmodulesRingBasis.mul, image_op_mul, mul_subset_mul, IsCompact.mul, mul_iInter_subset, RingSubgroupsBasis.mul, Ioi_mul_Ici_subset', Submonoid.coe_mul_self_eq, subset_mul_left, mul_mem_mul, mem_mul, singleton_mul_singleton, subset_interior_mul_right, LowerSet.coe_mul, star_mul, inter_mul_union_subset_union, subgroupClosure_mul, AddSubmonoid.closure_mul_closure, Finset.support_mulAntidiagonal_subset_mul, singleton_mul_ball, list_prod_subset_list_prod, one_mem_inv_mul_iff, exists_mem_nhds_zero_mul_subset, Filter.HasBasis.mul, subset_interior_mul, AddSubmonoid.mul_eq_closure_mul_set, MeasureTheory.measure_mul_closure_one
|
mulOneClass 📖 | CompOp | 4 mathmath: Finset.coeMonoidHom_apply, Finset.coe_coeMonoidHom, singletonMonoidHom_apply, coe_singletonMonoidHom
|
neg 📖 | CompOp | 146 mathmath: ball_sub, neg_Ioo, Convex.neg, mem_neg, neg_Ioi, IsDiscrete.exists_nhds_eq_zero_of_image_addLeft_inter_nonempty, inter_neg, HasCompactSupport.convolution_integrand_bound_left, neg_Icc, smul_set_neg, BddBelow.neg, image_neg_of_apply_neg_eq, nonempty_image_addRight_neg_inter_iff, image_neg_eq_neg, derivWithin_comp_const_sub, Seminorm.neg_ball, IsGLB.neg, neg_uIcc, Bornology.isVonNBounded_neg, neg_eq_empty, convexHull_union_neg_eq_absConvexHull, exists_closed_nhds_zero_neg_eq_add_subset, bddAbove_neg, neg_ball, StrictConvex.neg, infEDist_neg_neg, sInter_neg, nonempty_image_addLeft_neg_inter_iff, balancedHull_subset_convexHull_union_neg, neg_subset_sub_right, encard_neg, neg_op_vadd_set_distrib, IsCompact.neg, MeasureTheory.measure_neg_null, neg_empty, Bornology.IsVonNBounded.neg, isLUB_neg', neg_thickening, AddSubgroup.neg_subset_closure, IsUpperSet.neg, Filter.neg_mem_neg, IsAddFreimanHom.neg, compl_neg, sInf_neg, neg_subset_neg, isGLB_neg, infEDist_neg, AddSubmonoid.coe_negOrderIso_symm_apply, ball_sub_zero, neg_prod, sUnion_neg, neg_cthickening, neg_smul, balanced_neg, AddSubgroup.closure_toAddSubmonoid, neg_Ici, AddSubmonoid.coe_neg, Real.sInf_neg, Cardinal.mk_neg, JoinedIn.neg, Finite.neg, IsTopologicalAddGroup.addNegClosureNhd.neg, BddAbove.neg, Nonempty.neg, neg_mem_nhds_zero, neg_coe_set, convexHull_neg, totallyBounded_neg, neg_setOf, Finset.coe_neg, exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add, Seminorm.neg_closedBall, isLUB_neg, zero_mem_neg_add_iff, iUnion_neg, neg_subset, neg_Ioc, neg_smul_set, MeasurableSet.neg, IsPathConnected.neg, natCard_neg, neg_Iio, MeasureTheory.Measure.measure_neg, image_neg_of_apply_neg_eq_neg, IsApproximateAddSubgroup.neg_eq_self, neg_preimage, sSup_neg, csInf_neg, AddSubmonoid.closure_neg, isGLB_neg', gauge_neg_set_eq_gauge_neg, neg_singleton, IsCompact.closedBall_zero_sub, iInter_neg, mem_vadd_set_neg, AddSubgroup.closure_neg, Bornology.IsBounded.neg, infinite_neg, Absorbs.neg_neg, Balanced.neg, gauge_neg_set_neg, neg_vadd_set_distrib, small_neg, neg_closedBall, infEdist_neg, smul_neg, zero_notMem_neg_add_iff, AddSubmonoid.mem_closure_neg, Filter.HasBasis.neg, IsClosed.neg, IsLUB.neg, neg_range, bddBelow_neg, finite_neg, spectrum.neg_eq, MeasureTheory.eventuallyConst_neg_set_ae, AddSubmonoid.coe_negOrderIso_apply, neg_univ, nonempty_neg, Balanced.neg_eq, neg_insert, image_op_neg, ncard_neg, Real.sSup_neg, absorbs_neg_neg, neg_Iic, infEdist_neg_neg, IsDiscrete.exists_nhds_eq_zero_of_image_addRight_inter_nonempty, neg_closure, neg_Ico, Real.sInf_def, StarConvex.neg, MeasureTheory.Measure.neg_apply, HasCompactSupport.convolution_integrand_bound_right, Submodule.coe_set_neg, Submodule.span_neg_eq_neg, union_neg, Submodule.span_neg, MapsTo.neg, derivWithin_comp_neg, IsLowerSet.neg, neg_mem_neg, neg_pi, IsOpen.neg, csSup_neg, image_neg
|
one 📖 | CompOp | 53 mathmath: upperClosure_one, Finset.coe_one, finite_one, group_inseparable_iff, lowerClosure_one, SetSemiring.down_one, coe_singletonOneHom, mem_prod_list_ofFn, mem_one, Metric.ediam_one, csSup_one, Filter.le_one_iff, image_one, preimage_mul_left_one, image_list_prod, mul_eq_one_iff, Filter.one_mem_one, NonemptyInterval.coe_one, one_nonempty, sInf_one, SetSemiring.one_def, Nonempty.subset_one_iff, Ideal.span_one, sSup_one, Interval.coe_one, Finset.coe_list_prod, one_prod_one, Submodule.one_eq_span_one_set, list_prod_singleton, preimage_mul_right_one, one_subset, csInf_one, AddSubmonoid.one_eq_closure_one_set, coe_set_eq_one, SubMulAction.subset_coe_one, up_one, Finset.coe_eq_one, small_set_one, EMetric.diam_one, mem_list_prod, image_op_one, toFinset_one, preimage_mul_right_one', list_prod_mem_list_prod, Filter.principal_one, QuotientGroup.image_coe, Metric.diam_one, one_mem_one, subset_one_iff_eq, singleton_one, preimage_mul_left_one', Finite.toFinset_one, list_prod_subset_list_prod
|
semigroup 📖 | CompOp | — |
singletonAddHom 📖 | CompOp | 2 mathmath: coe_singletonAddHom, singletonAddHom_apply
|
singletonAddMonoidHom 📖 | CompOp | 2 mathmath: singletonAddMonoidHom_apply, coe_singletonAddMonoidHom
|
singletonMonoidHom 📖 | CompOp | 2 mathmath: singletonMonoidHom_apply, coe_singletonMonoidHom
|
singletonMulHom 📖 | CompOp | 2 mathmath: singletonMulHom_apply, coe_singletonMulHom
|
singletonOneHom 📖 | CompOp | 1 mathmath: coe_singletonOneHom
|
singletonZeroHom 📖 | CompOp | 1 mathmath: coe_singletonZeroHom
|
sub 📖 | CompOp | 119 mathmath: singleton_sub_closedBall_zero, ball_sub, sub_nonempty, union_sub_inter_subset_union, singleton_sub_ball, Filter.le_sub_iff, Balanced.sub, closedBall_sub_singleton, iUnion_sub_left_image, sub_sInter_subset, closedBall_sub_ball, finite_sub, sub_subset_sub_right, sub_subset_range, Nonempty.sub, preimage_sub, sub_singleton, image_sub, sub_iInter₂_subset, image2_sub, IsLowerSet.sub_left, ruzsa_covering_add, Filter.mem_sub, Finset.coe_sub, neg_subset_sub_right, sub_image_prod, vadd_sub_vadd_comm, infinite_sub, IsLUB.sub, small_sub, empty_sub, preimage_sub_preimage_subset, sub_iUnion₂, sInf_sub, sub_inter_subset, Bornology.isVonNBounded_sub_of_nonempty, mem_sub, MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos, LowerSet.coe_sub, StarConvex.sub, ball_sub_zero, sub_subset_iff, singleton_sub, sInter_sub_subset, IsLowerSet.sub_right, Finite.sub, closedBall_zero_sub_singleton, subset_interior_sub, IsOpen.sub_closure, IsUpperSet.sub_left, singleton_sub_singleton, subset_sub_left, IsOpen.closure_sub, Absorbs.sub, iInter₂_sub_subset, sub_subset_sub_left, Bornology.IsVonNBounded.sub, sub_eq_empty, MapsTo.sub, IsCompact.sub_closedBall_zero, IsGLB.sub, isBounded_sub, union_sub, Bornology.IsBounded.sub, spectrum.singleton_sub_eq, BoundedSub.isBounded_sub, singleton_sub_ball_zero, IsOpen.sub_right, UpperSet.coe_sub, IsCompact.sub_closedBall, Bornology.isVonNBounded_sub, sub_iUnion, sSup_sub, subset_interior_sub_left, sub_empty, IsCompact.closedBall_zero_sub, iInter_sub_subset, Filter.sub_mem_sub, IsUpperSet.sub_right, MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos_ne_top, sub_sUnion, zero_notMem_sub_iff, coe_sub_coe, Filter.HasBasis.sub, sub_subset_sub, IsAddFreimanHom.sub, ball_zero_sub_singleton, iUnion_sub_right_image, iUnion₂_sub, csInf_sub, sub_ball_zero, StrictConvex.sub, sub_mem_sub, convexHull_sub, Convex.sub, inter_sub_subset, sub_iInter_subset, zero_mem_sub_iff, AddAction.stabilizer_subset_sub_right, sub_union, sUnion_sub, csSup_sub, closedBall_sub_closedBall, ball_sub_ball, iUnion_sub, ConvexCone.IsReproducing.sub_eq_univ, ball_sub_singleton, IsOpen.sub_left, singleton_sub_closedBall, Disjoint.zero_notMem_sub_set, sub_ball, Nonempty.zero_mem_sub, inter_sub_union_subset_union, spectrum.sub_singleton_eq, ball_sub_closedBall, natCard_sub_le, univ_sub_univ, Cardinal.mk_sub_le, subset_interior_sub_right
|
subtractionCommMonoid 📖 | CompOp | — |
subtractionMonoid 📖 | CompOp | — |
zero 📖 | CompOp | 85 mathmath: preimage_add_right_zero, mem_list_sum, Nonempty.zero_smul, upperClosure_zero, preimage_add_right_zero', instNoZeroDivisors, absorbs_zero_iff, mem_sum_list_ofFn, zero_smul_subset, coe_singletonZeroHom, subset_zero_iff_eq, zero_prod_zero, mul_zero_subset, list_sum_singleton, ConvexCone.coe_zero, csInf_zero, egauge_zero_zero, Metric.ediam_zero, gauge_zero', zero_nonempty, small_set_zero, HomogeneousIdeal.coe_bot, egauge_zero_left, toFinset_zero, list_sum_subset_list_sum, ProperCone.innerDual_zero, NonemptyInterval.coe_zero, Finset.coe_eq_zero, Interval.coe_zero, Filter.nonpos_iff, convex_list_sum, finite_zero, inv_zero, gauge_closure_zero, coe_set_eq_zero, Nonempty.smul_zero, egauge_zero_left_eq_top, MvPolynomial.restrictSupport_zero, lowerClosure_zero, ProperCone.dual_zero, zero_smul_set, PointedCone.dual_zero, convexHull_eq_zero, zero_mem_zero, mem_zero, sInf_zero, zero_subset, Nonempty.zero_mul, preimage_add_left_zero', zero_mul_subset, image_zero, QuotientAddGroup.image_coe, Finset.coe_zero, convexHull_zero, Nonempty.subset_zero_iff, Ideal.span_zero, Nonempty.div_zero, Absorbs.zero, add_eq_zero_iff, list_sum_mem_list_sum, smul_zero_subset, Filter.principal_zero, tangentConeAt_subset_zero, Nonempty.zero_div, EMetric.diam_zero, Nonempty.mul_zero, preimage_add_left_zero, convexHull_list_sum, zero_div_subset, div_zero_subset, Metric.diam_zero, Submodule.span_zero, Finset.coe_list_sum, image_list_sum, image_op_zero, convex_zero, sSup_zero, addGroup_inseparable_iff, csSup_zero, Finite.toFinset_zero, zero_smul_set_subset, ConvexBody.coe_zero, Filter.zero_mem_zero, singleton_zero, balanced_zero
|