| Name | Category | Theorems |
|---|
instAdd 📖 | CompOp | 182 mathmath: AddHom.coe_prodMap, WithCStarModule.add_fst, IsAddLeftRegular.sumMk, mk_add_mk, RingEquiv.coe_prodComm_symm, AddHom.prod_map_comap_prod', Finsupp.sumFinsuppLEquivProdFinsupp_apply, Complex.equivRealProdAddHom_symm_apply, NumberField.mixedEmbedding.convexBodySumFun_add_le, AddEquiv.prodUnique_apply, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl, RingEquiv.prodProdProdComm_apply, AddSubsemigroup.prod_eq_top_iff, ContMDiffAdd.prod, AddHom.comp_noncommCoprod, isIsometricVAdd'', AddEquiv.coe_prodComm_symm, RingEquiv.piOptionEquivProd_apply, RingEquiv.snd_comp_coe_prodComm, AddHom.coe_prod, fst_add_snd, OrderAddMonoidHom.addCommute_inlₗ_inrₗ, MulEquiv.prodMultiplicative_symm_apply, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, MeasureTheory.Measure.prod.instIsAddLeftInvariant, AddCommute.prod, Filter.Tendsto.uniformity_add_iff_right, AddSubsemigroup.coe_prod, AddEquiv.prodProdProdComm_apply, Set.prod_add_prod_comm, add_def, instIsLeftCancelAdd, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, AddHom.noncommCoprod_apply', MulEquiv.prodMultiplicative_apply, OrderAddMonoidHom.addCommute_inl_inr, AddEquiv.uniqueProd_symm_apply, orderedSub, Unitization.cobounded_eq_aux, DirectSum.addEquivProdDirectSum_symm_apply_toFun, Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply, instUniqueSums, RingEquiv.piEquivPiSubtypeProd_symm_apply, RingEquiv.prodZeroRing_symm_apply, AddCommGroup.equiv_free_prod_directSum_zmod, RingEquiv.zeroRingProd_symm_apply, AddEquiv.coe_prodAssoc, addSemiconjBy_iff, AddMonoidHom.noncommCoprod_unique, AddSubsemigroup.srange_snd, AddSubsemigroup.mem_prod, AddLocalization.r_of_eq, AddHom.prodMap_def, Set.addCenter_prod, IsModuleTopology.instProd, AddSubsemigroup.le_prod_iff, AddHom.prod_apply, AddSubsemigroup.top_prod_top, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, QuaternionAlgebra.coe_addEquivProd, AddEquiv.prodProdProdComm_toEquiv, QuadraticForm.dualProdIsometry_invFun, Filter.Tendsto.uniformity_add_iff_left, NumberField.mixedEmbedding.normAtPlace_add_le, AddLocalization.r_iff_exists, zero_mk_add_zero_mk, RingEquiv.piEquivPiSubtypeProd_apply, Finsupp.snd_sumFinsuppAddEquivProdFinsupp, Complex.equivRealProdAddHom_symm_apply_re, Ideal.quotientMulEquivQuotientProd_snd, Complex.equivRealProdAddHom_symm_apply_im, Ideal.fst_comp_quotientMulEquivQuotientProd, AddHom.prod_unique, MeasureTheory.Measure.prod.instIsAddRightInvariant, RingEquiv.prodCongr_apply, DirectSum.addEquivProdDirectSum_apply, Filter.Tendsto.uniformity_add, AddHom.coe_fst, DirectSum.addEquivProdDirectSum_symm_apply_support', instIsCancelAdd, AddSubsemigroup.bot_prod_bot, AddLocalization.zero_rel, Finsupp.sumFinsuppAddEquivProdFinsupp_apply, Finset.product_nsmul, AddEquiv.prodAdditive_apply, continuousAdd, RingEquiv.sumArrowEquivProdArrow_symm_apply, CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_fst, AddSubmonoid.LocalizationMap.eq', QuadraticForm.dualProdIsometry_toFun, AddEquiv.prodAdditive_symm_apply, RingEquiv.prodZeroRing_apply, DFinsupp.equivProdDFinsupp_add, AddEquiv.coe_prodComm, AddLocalization.mk_eq_mk_iff, Ideal.snd_comp_quotientMulEquivQuotientProd, AddEquiv.coe_prodAssoc_symm, Ideal.quotientInfEquivQuotientProd_snd, RingEquiv.coe_prodComm, AddHom.comp_coprod, Finsupp.fst_sumFinsuppAddEquivProdFinsupp, RingEquiv.prodProdProdComm_toMulEquiv, LieAlgebra.of_add, Complex.equivRealProdAddHom_apply, AddSemiconjBy.prod, instExistsAddOfLE, RingEquiv.prodProdProdComm_symm, AddMonoidAlgebra.curryRingEquiv_symm_single, OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex, instCanonicallyOrderedAdd, Ideal.quotientMulEquivQuotientProd_fst, QuaternionAlgebra.coe_symm_addEquivProd, addAddHom_apply, isAddRegular_mk, AddSubsemigroup.top_prod, Unitization.isUniformEmbedding_addEquiv, AddHom.fst_comp_prod, RingEquiv.coe_prodCongr, fst_add, RingEquiv.zeroRingProd_apply, IsAddRightRegular.sumMk, Set.addCentralizer_prod, AddMonoidHom.addCommute_inl_inr, RingEquiv.sumArrowEquivProdArrow_apply, LinearEquiv.prodAssoc_apply, AddSubsemigroup.prod_mono, AddLocalization.r_iff_oreEqv_r, Ideal.quotientInfEquivQuotientProd_fst, OrderAddMonoidHom.inl_add_inr_eq_mk, mk_zero_add_mk_zero, AddHom.coprod_apply, RingEquiv.piFinTwo_symm_apply, Set.prod_addCentralizer_subset_addCentralizer_prod, CategoryTheory.Abelian.Ext.addEquivBiprod_symm_apply, Unitization.antilipschitzWith_addEquiv, WithCStarModule.add_snd, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr, addAddMonoidHom_apply, AddMonoidAlgebra.curryRingEquiv_single, AddEquiv.prodUnique_symm_apply, swap_add, AddHom.coe_snd, Set.nsmul_prod, addCommute_iff, Ideal.fst_comp_quotientInfEquivQuotientProd, Ideal.map_prodComm_prod, Unitization.uniformity_eq_aux, LieAlgebra.of_symm_add, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_snd, Unitization.lipschitzWith_addEquiv, AddSubsemigroup.srange_fst, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, instTwoUniqueSums, Ideal.snd_comp_quotientInfEquivQuotientProd, Finset.product_add_product_comm, CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply, vaddCommClassBoth, RingEquiv.piOptionEquivProd_symm_apply, RingEquiv.piFinTwo_apply, RingEquiv.prodProdProdComm_toEquiv, RingEquiv.fst_comp_coe_prodComm, AddEquiv.uniqueProd_apply, RingEquiv.prodProdProdComm_toAddEquiv, snd_add, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_fst, isAddLeftRegular_mk, AddHom.snd_comp_prod, AddHom.prod_comp_prodMap, CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_snd, DirectSum.lequivProdDirectSum_symm_apply, AddHom.noncommCoprod_apply, isAddRightRegular_mk, instIsRightCancelAdd, DoubleCentralizer.add_toProd, RingEquiv.prodCongr_symm_apply, AddSubsemigroup.prod_top, DirectSum.lequivProdDirectSum_apply, NonemptyInterval.toProd_add, isIsometricVAdd', LinearEquiv.prodProdProdComm_toAddEquiv, IsAddRegular.sumMk
|
instDiv 📖 | CompOp | 6 mathmath: snd_div, swap_div, fst_div, mk_div_mk, Filter.Tendsto.uniformity_div, div_def
|
instInv 📖 | CompOp | 9 mathmath: inv_mk, Filter.Tendsto.uniformity_inv_iff, continuousInv, Set.inv_prod, Filter.Tendsto.uniformity_inv, Finset.inv_product, fst_inv, snd_inv, swap_inv
|
instMul 📖 | CompOp | 152 mathmath: MulHom.coe_snd, LinearMap.inl_map_mul, Subsemigroup.srange_snd, ContMDiffMul.prod, Localization.one_rel, OrderMonoidHom.inl_mul_inr_eq_mk, MulHom.comp_coprod, RingEquiv.coe_prodComm_symm, MulEquiv.prodProdProdComm_apply, commute_iff, instCanonicallyOrderedMul, Finset.product_pow, MulHom.coe_fst, fst_mul_snd, smulMulHom_apply, instUniqueProds, RingEquiv.prodProdProdComm_apply, IsRightRegular.prodMk, semiconjBy_iff, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, SemiconjBy.prod, RingEquiv.piOptionEquivProd_apply, MulHom.coe_prodMap, RingEquiv.snd_comp_coe_prodComm, MulHom.prodMap_def, MulHom.coe_prod, MulEquiv.prodMultiplicative_symm_apply, Commute.prod, instPNatPowAssoc, isScalarTowerBoth, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, MulEquiv.prodMultiplicative_apply, Set.centralizer_prod, Subsemigroup.coe_prod, swap_mul, MulHom.prod_unique, RingEquiv.piEquivPiSubtypeProd_symm_apply, OrderMonoidHom.commute_inl_inr, RingEquiv.prodZeroRing_symm_apply, Set.prod_mul_prod_comm, RingEquiv.zeroRingProd_symm_apply, MeasureTheory.Measure.prod.instIsMulRightInvariant, MulEquiv.coe_prodAssoc, MulEquiv.prodUnique_symm_apply, MulEquiv.coe_prodComm_symm, Subsemigroup.mem_prod, MonoidHom.noncommCoprod_unique, instExistsMulOfLE, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, RingEquiv.piEquivPiSubtypeProd_apply, Localization.r_of_eq, Ideal.quotientMulEquivQuotientProd_snd, Ideal.fst_comp_quotientMulEquivQuotientProd, MulEquiv.prodUnique_apply, MulEquiv.prodProdProdComm_toEquiv, MonoidAlgebra.curryRingEquiv_symm_single, MulHom.prod_apply, RingEquiv.prodCongr_apply, Subsemigroup.prod_top, MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit, snd_mul, MeasureTheory.Measure.prod.instIsMulLeftInvariant, isRegular_mk, mul_def, Subsemigroup.srange_fst, isIsometricSMul'', MulEquiv.uniqueProd_symm_apply, AddEquiv.prodAdditive_apply, MulHom.noncommCoprod_apply, instIsLeftCancelMul, RingEquiv.sumArrowEquivProdArrow_symm_apply, fst_mul, CommGroup.equiv_free_prod_prod_multiplicative_zmod, AddEquiv.prodAdditive_symm_apply, RingEquiv.prodZeroRing_apply, MulEquiv.uniqueProd_apply, Set.center_prod, isLeftRegular_mk, Subsemigroup.top_prod, Ideal.snd_comp_quotientMulEquivQuotientProd, mulMonoidHom_apply, SemidirectProduct.mulEquivProd_symm_apply_left, Ideal.quotientInfEquivQuotientProd_snd, RingEquiv.coe_prodComm, Localization.r_iff_exists, isRightRegular_mk, RingEquiv.prodProdProdComm_toMulEquiv, Finset.product_mul_product_comm, MonoidHom.commute_inl_inr, MulEquiv.coe_prodAssoc_symm, OrderMonoidHom.commute_inlₗ_inrₗ, IsLeftRegular.prodMk, MulHom.snd_comp_prod, NumberField.mixedEmbedding.unitSMul_smul, instTwoUniqueProds, RingEquiv.prodProdProdComm_symm, MulHom.fst_comp_prod, MonoidAlgebra.curryRingEquiv_single, Set.prod_pow, mk_one_mul_mk_one, Submonoid.LocalizationMap.eq', Ideal.quotientMulEquivQuotientProd_fst, NonemptyInterval.toProd_mul, smulCommClassBoth, commProb_prod, MulEquiv.prodProdProdComm_symm, Filter.Tendsto.uniformity_mul, MulHom.noncommCoprod_apply', smulMonoidHom_apply, MulHom.prod_map_comap_prod', Filter.Tendsto.uniformity_mul_iff_right, RingEquiv.coe_prodCongr, RingEquiv.zeroRingProd_apply, mk_mul_mk, RingEquiv.sumArrowEquivProdArrow_apply, Ideal.quotientInfEquivQuotientProd_fst, mulMulHom_apply, RingEquiv.piFinTwo_symm_apply, IsRegular.prodMk, SemidirectProduct.mulEquivProd_apply, Subsemigroup.bot_prod_bot, isIsometricSMul', instIsRightCancelMul, SemidirectProduct.mulEquivProd_symm_apply_right, Subsemigroup.prod_eq_top_iff, MulHom.prod_comp_prodMap, Set.prod_centralizer_subset_centralizer_prod, Localization.r_iff_oreEqv_r, Ideal.fst_comp_quotientInfEquivQuotientProd, Ideal.map_prodComm_prod, MulHom.comp_noncommCoprod, Subsemigroup.prod_mono, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, Ideal.snd_comp_quotientInfEquivQuotientProd, Subsemigroup.top_prod_top, RingEquiv.piOptionEquivProd_symm_apply, RingEquiv.piFinTwo_apply, Subsemigroup.le_prod_iff, RingEquiv.prodProdProdComm_toEquiv, MonoidWithZeroHom.commute_inl_inr, RingEquiv.fst_comp_coe_prodComm, RingEquiv.prodProdProdComm_toAddEquiv, Filter.Tendsto.uniformity_mul_iff_left, LinearMap.inr_map_mul, MulHom.coprod_apply, NumberField.mixedEmbedding.logMap_mul, instIsCancelMul, MulEquiv.coe_prodComm, RingEquiv.prodCongr_symm_apply, continuousMul, Localization.mk_eq_mk_iff, one_mk_mul_one_mk
|
instNeg 📖 | CompOp | 18 mathmath: WithCStarModule.neg_fst, snd_neg, WithCStarModule.neg_snd, Filter.Tendsto.uniformity_neg, NumberField.mixedEmbedding.convexBodySum_neg_mem, neg_mk, fst_neg, Set.neg_prod, NumberField.mixedEmbedding.convexBodySumFun_neg, DoubleCentralizer.neg_toProd, Finset.neg_product, Filter.Tendsto.uniformity_neg_iff, NumberField.mixedEmbedding.convexBodyLT_neg_mem, NumberField.mixedEmbedding.normAtPlace_neg, Int.neg_mem_divisorsAntidiag, continuousNeg, NumberField.mixedEmbedding.convexBodyLT'_neg_mem, swap_neg
|
instOne 📖 | CompOp | 20 mathmath: Function.mulSupport_prodMk, NumberField.mixedEmbedding.logMap_one, Localization.one_rel, Finset.product_pow, instZeroLEOneClass, Filter.one_prod_one, NonemptyInterval.toProd_one, mk_eq_one, Set.one_prod_one, mk_one_one, Set.prod_pow, one_eq_mk, normOneClass, NumberField.mixedEmbedding.logMap_real, DoubleCentralizer.one_toProd, snd_one, Finset.one_product_one, fst_one, Function.mulSupport_prodMk', swap_one
|
instPow 📖 | CompOp | 14 mathmath: instNatPowAssoc, instPNatPowAssoc, NonemptyInterval.toProd_pow, pow_mk, DoubleCentralizer.pow_toProd, pow_def, pow_snd, instIsReducedProd, pow_swap, CFC.nnrpow_eq_nnrpow_prod, not_isCyclic_prod_of_infinite_nontrivial, Group.isCyclic_prod_iff, pow_fst, CFC.rpow_eq_rpow_prod
|
instSMul 📖 | CompOp | 94 mathmath: smulCommClass, MulActionHom.prod_apply, faithfulSMulRight, egauge_prod_mk, DFinsupp.equivProdDFinsupp_smul, WithLp.isBoundedSMulSeminormedAddCommGroupToProd, isCentralScalar, isSMulRegular_iff, image_mk_openSegment_left, NonemptyInterval.toProd_nsmul, extremePoints_prod, LieAlgebra.of_smul, WithLp.smul_snd, Asymptotics.isLittleOTVS_prodMk_left, segment_subset, Asymptotics.IsLittleOTVS.prodMk, DoubleCentralizer.smul_toProd, instSMulCommClassMatrixFinOfNatNatProd, smul_uniformity₀, WithCStarModule.smul_fst, StarConvex.prod, CliffordAlgebra.foldr'Aux_foldr'Aux, isScalarTowerBoth, NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, MulActionHom.prodMap_apply, ConcaveOn.convex_strict_hypograph, ConvexOn.openSegment_subset_strict_epigraph, MulActionHom.fst_apply, image_mk_segment_left, subset_tangentConeAt_prod_right, subset_tangentConeAt_prod_left, IsModuleTopology.instProd, AddGroup.isAddCyclic_prod_iff, NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.logMap_real_smul, ConvexOn.convex_epigraph, smul_mk_zero, instIsIsometricSMul, instPosSMulReflectLE, continuousConstSMul, openSegment_subset, Asymptotics.IsBigOTVS.prodMk, image_mk_openSegment_right, ConcaveOn.convex_hypograph, MulActionHom.snd_comp_prod, image_mk_segment_right, NumberField.mixedEmbedding.norm_smul, ConvexOn.convex_re_epigraph, le_egauge_prod, WithLp.normSMulClassSeminormedAddCommGroupToProd, smul_def, Convex.prod, ConcaveOn.openSegment_subset_strict_hypograph, instNormSMulClass, smul_swap, instSMulPosStrictMono, continuousSMul, WithLp.smul_fst, faithfulSMulLeft, instSMulPosReflectLE, WithLp.instProdNormSMulClass, IsUnit.smul_uniformity, smulCommClassBoth, NumberField.mixedEmbedding.convexBodyLT_convex, instPosSMulMono, NumberField.mixedEmbedding.logMap_real, smul_snd, MulActionHom.snd_apply, instIsBoundedSMul, NumberField.mixedEmbedding.normAtPlace_smul, ConvexOn.convex_strict_epigraph, Set.smul_set_prod, smul_uniformity, smul_mk, MulActionHom.prod_fst_snd, isScalarTower, NumberField.mixedEmbedding.convexBodySum_convex, instSMulPosReflectLT, NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem, instProperConstSMulProd, MulActionHom.fst_comp_prod, concaveOn_iff_convex_hypograph, Asymptotics.isBigOTVS_prodMk_left, WithCStarModule.smul_snd, smul_zero_mk, WithLp.instProdIsBoundedSMul, LieAlgebra.of_symm_smul, instStarModule, WithCStarModule.prod_inner, instSMulPosMono, convexOn_iff_convex_epigraph, instPosSMulStrictMono, NumberField.mixedEmbedding.convexBodyLT'_convex, smul_fst
|
instStar 📖 | CompOp | 35 mathmath: NonUnitalStarSubalgebra.prod_toNonUnitalSubalgebra, NonUnitalStarAlgHom.inl_apply, StarAlgHom.prodEquiv_apply, NonUnitalStarAlgHom.prodEquiv_symm_apply, StarAlgHom.snd_apply, StarAlgHom.coe_prod, NonUnitalStarAlgHom.prod_fst_snd, NonUnitalStarAlgHom.prod_apply, NonUnitalStarAlgHom.inr_apply, StarAlgHom.snd_prod, NonUnitalStarAlgHom.snd_apply, NonUnitalStarAlgHom.prodEquiv_apply, NonUnitalStarSubalgebra.prod_mono, StarAlgHom.prod_fst_snd, star_def, NonUnitalStarAlgHom.fst_apply, NonUnitalStarSubalgebra.prod_inf_prod, instTrivialStar, NonUnitalStarAlgHom.fst_prod, StarAlgHom.prod_apply, instContinuousStarProd, NonUnitalStarAlgHom.coe_prod, StarAlgHom.prodEquiv_symm_apply, NonUnitalStarSubalgebra.coe_prod, Units.embed_product_star, NonUnitalStarAlgHom.snd_prod, NonUnitalStarAlgHom.coe_inr, StarAlgHom.fst_prod, snd_star, NonUnitalStarAlgHom.coe_inl, NonUnitalStarSubalgebra.prod_top, fst_star, instStarModule, NonUnitalStarSubalgebra.mem_prod, StarAlgHom.fst_apply
|
instSub 📖 | CompOp | 14 mathmath: HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, orderedSub, WithCStarModule.sub_snd, HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub, HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal, mk_sub_mk, DoubleCentralizer.sub_toProd, Filter.Tendsto.uniformity_sub, HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub, swap_sub, WithCStarModule.sub_fst, sub_def, snd_sub, fst_sub
|
instVAdd 📖 | CompOp | 24 mathmath: AddActionHom.fst_comp_prod, AddActionHom.snd_apply, vaddCommClass, faithfulVAddRight, Set.vadd_set_prod, faithfulVAddLeft, vadd_mk, vadd_def, vadd_snd, AddActionHom.snd_comp_prod, vadd_swap, AddActionHom.fst_apply, continuousConstVAdd, continuousVAdd, vaddAssocClass, isCentralVAdd, vadd_uniformity, AddActionHom.prodMap_apply, AddActionHom.prod_fst_snd, IsAddUnit.vadd_uniformity, vadd_fst, AddActionHom.prod_apply, vaddCommClassBoth, instIsIsometricVAdd
|
instZero 📖 | CompOp | 42 mathmath: fst_zero, NumberField.mixedEmbedding.norm_eq_zero_iff', WithLp.isBoundedSMulSeminormedAddCommGroupToProd, Set.zero_prod_zero, Asymptotics.isLittleOTVS_prodMk_left, instZeroLEOneClass, Asymptotics.IsLittleOTVS.prodMk, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, Nat.unpair_zero, Finset.zero_product_zero, mk_zero_zero, NonemptyInterval.toProd_zero, Function.support_prodMk, WithCStarModule.zero_snd, swap_zero, Asymptotics.IsBigOTVS.prodMk, AddLocalization.zero_rel, Finset.product_nsmul, Function.support_prodMk', LieAlgebra.of_zero, Filter.zero_prod_zero, instSMulPosStrictMono, mk_eq_zero, zero_eq_mk, instSMulPosReflectLE, NumberField.mixedEmbedding.forall_normAtPlace_eq_zero_iff, SchwartzMap.schwartzSeminormFamily_apply_zero, NumberField.mixedEmbedding.unit_smul_eq_zero, DoubleCentralizer.zero_toProd, LieAlgebra.of_symm_zero, instIsBoundedSMul, instIsReducedProd, WithCStarModule.zero_fst, instSMulPosReflectLT, Set.nsmul_prod, MeasureTheory.SimpleFunc.FinMeasSupp.pair, Asymptotics.isBigOTVS_prodMk_left, NumberField.mixedEmbedding.logMap_zero, instSMulPosMono, PerfectClosure.mk_zero, snd_zero, NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff
|