univ π | CompOp | 1635 mathmath: map_nsmul_piAntidiag_univ, ArithmeticFunction.vonMangoldt.residueClass_eq, Fintype.card_pi, Fin.prod_univ_four, Fintype.univ_empty, NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', ContinuousLinearMap.sum_comp_single, WittVector.remainder_vars, Behrend.sum_lt, insert_compl_self, Fintype.prod_sigma', Submonoid.mem_closure_iff_of_fintype, exists_continuous_sum_one_of_isOpen_isCompact, Fin.univ_map_def, Fintype.sum_empty, PiLp.nndist_eq_sum, ContinuousLinearMap.isPositive_iff_eq_sum_rankOne, Fin.prod_univ_getElem, CategoryTheory.Abelian.Ext.comp_sum, SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq, univ_prod_mulSingle, Set.Finite.toFinset_setOf, RootPairing.posRootForm_posForm_apply_apply, HasFDerivWithinAt.continuousMultilinearMap_apply, Fintype.prod_fiberwise', cfc_sum_univ, Monovary.sum_mul_comp_perm_eq_sum_mul_iff, norm_torusIntegral_le_of_norm_le_const, Matrix.det_apply, OrthonormalBasis.orthogonalProjection_eq_sum, univ_infs_univ, Fin.prod_univ_five, Finsupp.degree_eq_sum, sym_univ, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, MeasureTheory.Integrable.fin_nat_prod, Fintype.coe_image_univ, mem_univ, RootPairing.Polarization_apply, Fintype.prod_dite, card_univ, SimpleGraph.lapMatrix_toLinearMapβ', Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, MeasureTheory.lmarginal_univ, AddDissociated.randomisation, Fintype.prod_option, NumberField.InfinitePlace.sum_mult_eq, hasStrictFDerivAt_list_prod_finRange', ContinuousMultilinearMap.map_smul_univ, IsCyclic.image_range_orderOf, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, Fintype.one_le_prod, sum_col_of_mem_doublyStochastic, AlgebraicTopology.NormalizedMooreComplex.obj_d, toLeft_eq_univ, sum_centroidWeightsIndicator_eq_one_of_nonempty, MultilinearMap.mkPiAlgebra_apply, ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le, centroid_eq_affineCombination_fintype, EuclideanSpace.closedBall_zero_eq, map_finset_sum, Module.Basis.equivFun_symm_apply, AkraBazziRecurrence.tendsto_zero_sumCoeffsExp, Set.powersetCard.val_ofFinEmb, Fintype.sum_unique, Fin.sum_univ_castSucc, eq_univ_iff_forall, Complex.integral_comp_pi_polarCoord_symm, univ_pi_univ, ContinuousMultilinearMap.norm_map_snoc_le, Tuple.lt_card_lt_iff_apply_lt_of_monotone, inf'_univ_eq_ciInf, image_orderEmbOfFin_univ, attach_eq_univ, AddMonoidHom.noncommPiCoprod_apply, prod_fin_eq_prod_range, SimpleGraph.two_mul_card_edgeFinset, Affine.Simplex.inv_height_eq_sum_mul_inv_dist, OrthonormalBasis.sum_inner_mul_inner, prod_eq_prod_extend, ContinuousMultilinearMap.alternatization_apply_apply, Colex.toColex_univ, univ_disjSum_univ, SimpleGraph.sum_degrees_eq_twice_card_edges, Fin.prod_univ_eight, compl_eq_univ_sdiff, Nat.sumByResidueClasses, vadd_finset_eq_univ, AddSubgroup.mem_closure_range_iff_of_fintype, MeasureTheory.integral_fintype_prod_volume_eq_pow, IntermediateField.coe_prod, Pi.card_Ici, ZMod.invDFT_apply, neg_filter_univ, supIndep_univ_fin_two, SzemerediRegularity.a_add_one_le_four_pow_parts_card, SimpleGraph.sum_incMatrix_apply, Equiv.Perm.card_of_cycleType_mul_eq, FinVec.prod_eq, Finsupp.sum_zsmul, Affine.Simplex.face_centroid_eq_iff, Nat.mem_finMulAntidiag, LieModule.traceForm_eq_sum_finrank_nsmul', Fintype.expect_mul_expect, LinearMap.det_pi, Fintype.piFinset_univ, List.alternatingProd_eq_finset_prod, MeasureTheory.Measure.pi'_pi, AddMonoidHom.card_fiber_eq_of_mem_range, SimpleGraph.Dart.edge_fiber, sum_hom_units, ContinuousMultilinearMap.mkPiAlgebra_apply, EuclideanSpace.norm_sq_eq, Fintype.sum_ite_eq', Fintype.sum_eq_zero, AkraBazziRecurrence.tendsto_atTop_sumCoeffsExp, Pi.norm_def', Matrix.trace_blockDiagonal', Monovary.sum_mul_sum_le_card_mul_sum, Affine.Simplex.centroid_eq_smul_sum_vsub_vadd, SimpleGraph.dotProduct_mulVec_adjMatrix, Fin.image_succ_univ, Monovary.sum_smul_comp_perm_le_sum_smul, Fin.sum_neg_one_pow, IsCompl.sum_add_sum, AddChar.sum_mulShift, sum_fiberwise', ContinuousAlternatingMap.le_mul_prod_of_opNorm_le_of_le, OrderedFinpartition.norm_compAlongOrderedFinpartition_le, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, sum_smul_minpolyDiv_eq_X_pow, Matrix.sum_single_one, MeasureTheory.integral_fintype_prod_eq_prod, Fintype.prod_eq_one, Fintype.expect_dite_eq, ProbabilityTheory.Kernel.sum_fintype, OrderedFinpartition.norm_applyOrderedFinpartition_le, Matrix.det_vandermonde, Fin.univ_image_getElem', Fintype.prod_equiv, CategoryTheory.Abelian.Ext.sum_comp, Fintype.mem_span_image_iff_exists_fun, ProbabilityTheory.sum_meas_smul_cond_fiber, Pi.addOrderOf, Fin.prod_ofFn, Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe, mem_doublyStochastic_iff_sum, IsAddCyclic.image_range_addOrderOf, Matrix.linfty_opNorm_replicateRow, SimpleGraph.dart_edge_fiber_card, Sym.coe_equivNatSumOfFintype_apply_apply, InnerProductSpace.canonicalCovariantTensor_eq_sum, Function.Embedding.exists_of_card_eq_finset, AlternatingMap.domCoprod_coe, Fin.prod_univ_fun_getElem, Affine.Triangle.prod_dist_div_dist_eq_one_of_mem_line_of_mem_line, Submodule.mem_span_image_iff_exists_fun, univ_sum_single, HasFDerivWithinAt.linear_multilinear_comp, Set.toFinset_range, Polynomial.ofFn_eq_sum_monomial, Equiv.finsuppUnique_symm_apply_support_val, MeasureTheory.lintegral_prod_lintegral_pow_le, Pi.card_Iic, Matrix.det_succ_row, Fintype.expect_eq_zero_iff_of_nonpos, smul_finset_univ, image_univ_equiv, card_eq_iff_eq_univ, mulEnergy_univ_left, Matrix.sum_hadamard_eq, sum_fin_eq_sum_range, coe_univ, ContinuousMultilinearMap.mkPiRing_apply, Matrix.det_eq_sum_mul_adjugate_row, Multiset.sum_toEnumFinset, mulEnergy_univ_right, Affine.Simplex.univ_centroid_eq, union_compl, Behrend.sum_sq_le_of_mem_box, Matrix.matrix_eq_sum_single, univ_filter_exists, Sum.Lex.Iic_inr, Fin.sum_sum_eq_sum_triangle_add, Function.Bijective.sum_comp, Composition.sum_blocksFun, hasProd_fintype, Set.mem_nsmul_iff_sum, OrthonormalBasis.sum_sq_inner_right, Monovary.sum_comp_perm_mul_le_sum_mul, MeasureTheory.volume_pi_pi, SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset, HasFDerivWithinAt.continuousAlternatingMap_apply, EuclideanSpace.nndist_eq, ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity, Ideal.finsuppTotal_apply_eq_of_fintype, NumberField.prod_abs_eq_one, Matrix.sum_sum_single, MultilinearMap.map_sum, Set.filter_mem_univ_eq_toFinset, Fin.prod_congr', Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst, Fintype.expect_ite_eq, Fintype.sum_pos, mem_image_univ_iff_mem_range, Matrix.det_projVandermonde, Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter, Multiset.bijective_iff_map_univ_eq_univ, Affine.Simplex.sum_mongePointWeightsWithCircumcenter, NumberField.mixedEmbedding.convexBodyLT_volume, Set.mem_fintype_prod, Fintype.card_filter_piFinset_eq, CategoryTheory.leftDistributor_hom, ZMod.completedLFunction_def_even, Complex.volume_sum_rpow_le, Fintype.prod_extend_by_one, Behrend.map_succ, PiLp.nnnorm_eq_of_L2, Behrend.map_le_of_mem_box, iteratedDeriv_scomp_eq_sum_orderedFinpartition, List.sum_ofFn, vadd_finset_univ, AddChar.sum_eq_ite, MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum, Affine.Simplex.centroid_eq_of_range_eq, Fin.sum_univ_eq_sum_range, Module.Basis.det_isUnitSMul, Fintype.expect_ite_zero, filter_le_le_eq_Icc, HasFDerivAt.multilinear_comp, ContinuousMultilinearMap.linearDeriv_apply, Int.univ_addEquiv, HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top, SimpleGraph.odd_card_odd_degree_vertices_ne, Set.biUnion_finsetSigma_univ, AddSubgroup.exists_of_mem_closure_range, ContinuousAlternatingMap.le_opNNNorm, ContinuousMultilinearMap.le_of_opNNNorm_le, MeasureTheory.integral_fintype_prod_eq_pow, CuspForm.coe_trace, Fin.sum_snoc, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, NumberField.mixedEmbedding.convexBodySumFun_apply', AddSubgroup.index_iInf_le, Finsupp.univ_sum_single_apply', ContinuousMultilinearMap.map_sum, Orthonormal.inner_left_fintype, Monoid.exponent_pi, RCLike.wInner_cWeight_eq_expect, Matrix.toBilin_apply, Affine.Simplex.centroid_weighted_vsub_eq_zero, gaussSum_mul, Pi.sum_norm_apply_le_norm', MeasureTheory.charFunDual_pi', Fintype.expect_dite_eq', Equiv.Perm.sign_eq_prod_prod_Ioi, MultilinearMap.dfinsuppFamily_apply_support', Fintype.sum_ite_eq, Fin.card_filter_univ_succ, DirectSum.sum_univ_of, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, Fintype.prod_sigma, sum_attach_eq_sum_dite, CategoryTheory.Limits.IsBilimit.total, MeasureTheory.OuterMeasure.le_pi, Antivary.sum_mul_le_sum_comp_perm_mul, ZMod.LFunction_def_odd, HasStrictFDerivAt.list_prod', FiniteField.sum_pow_lt_card_sub_one, Affine.Simplex.inv_height_lt_sum_inv_height, Tuple.lt_card_gt_iff_apply_gt_of_antitone, ProbabilityTheory.iIndepFun.hasGaussianLaw_fun_sum, sum_indicator_mod, MeasureTheory.integral_fin_nat_prod_volume_eq_prod, Affine.Simplex.excenter_eq_affineCombination, LinearMap.sumOfConjugatesEquivariant_apply, Fintype.prod_mono', Fintype.one_lt_prod_iff_of_one_le, Fin.sum_univ_add, AddChar.sum_apply_eq_ite, ProbabilityTheory.iIndepSets.meas_iInter, piAntidiag_univ_fin_eq_antidiagonalTuple, MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, compl_singleton, Fintype.prod_prod_type_right, MeasureTheory.Measure.sum_fintype, MeasureTheory.Measure.pi_pi_aux, Nat.coprime_fintype_prod_left_iff, MeasureTheory.lintegral_eq_lmarginal_univ, AddChar.sum_eq_zero_iff_ne_zero, Matrix.charpoly_of_upperTriangular, Fin.univ_def, Equiv.sum_comp, Real.volume_pi_Ico, sup_univ_eq_ciSup, fderiv_continuousAlternatingMap_apply, SimpleGraph.neighborFinset_completeEquipartiteGraph, smul_finset_univβ, AddSubgroup.noncommPiCoprod_apply, Finsupp.sum_fintype, SimpleGraph.dotProduct_mulVec_degMatrix, FiniteField.roots_X_pow_card_sub_X, wittStructureRat_vars, AddAction.stabilizer_finset_univ, PiTensorProduct.ofFinsuppEquiv'_tprod_single, finSigmaFinEquiv_apply, Fintype.sum_pow, QuadraticMap.Ring.polarBilin_pi, Fintype.sum_eq_zero_iff_of_nonpos, ContinuousLinearMap.det_pi, mem_filter_univ, Multiset.Nat.mem_antidiagonalTuple, AlternatingMap.alternatizeUncurryFin_apply, addEnergy_univ_left, Fintype.sum_option, Matrix.toLinearMapβ'_apply, HasFDerivAt.continuousAlternatingMap_apply, Real.volume_Icc_pi, Fintype.sup_disjointed, Ideal.finrank_quotient_eq_sum, Icc_bot_top, AddChar.sum_eq_card_of_eq_one, DirichletCharacter.sum_characters_eq, Sym.coe_equivNatSumOfFintype_symm_apply, OrthonormalBasis.orthogonalProjection_apply_eq_sum, Polynomial.card_eq_of_natDegree_le_of_coeff_le, Fin.sum_trunc, ArithmeticFunction.vonMangoldt.residueClass_apply, univ_of_card_le_three, LinearMap.trace_eq_sum_inner, Fintype.sum_eq_add_sum_subtype_ne, Fin.sum_ofFn, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, singleton_eq_univ, NumberField.mulHeight_eq, Module.Basis.constrL_apply, Module.Basis.reindexFinsetRange_apply, Matrix.IsHermitian.charpoly_cfc_eq, addEnergy_eq_sum_sq, Affine.Triangle.prod_eq_prod_one_sub_of_mem_line_point_lineMap, MulAction.card_eq_sum_card_group_div_card_stabilizer, Fintype.IsSimpleOrder.univ, Fintype.sum_mono, univ_sups_univ, Matrix.card_GL_field, top_eq_univ, Fin.univ_succAbove, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, OrderedFinpartition.prod_sigma_eq_prod, Fin.prod_univ_succAbove, Algebra.norm_eq_prod_embeddings, Matrix.det_of_lowerTriangular, AddMonoid.exponent_eq_max'_addOrderOf, Fin.sum_univ_two', Function.Bijective.finset_sum, lintegral_comp_pi_polarCoord_symm, Fintype.sum_dite_eq', Fin.prod_univ_one, AddSubmonoid.exists_of_mem_closure_range, PiTensorProduct.projectiveSeminorm_tprod_le, subtype_eq_univ, AlternatingGroup.card_of_cycleType_singleton, finPiFinEquiv_apply, Affine.Simplex.ExcenterExists.excenter_eq_incenter_iff, Matrix.det_eq_sum_mul_adjugate_col, LinearMap.lsum_apply, extDeriv_apply_vectorField, CategoryTheory.Limits.biproduct.matrix_desc_assoc, DFinsupp.sum_eq_sum_fintype, Equiv.Perm.fixed_point_card_lt_of_ne_one, ProbabilityTheory.covariance_sum_right, Set.biInter_finsetSigma_univ, Fintype.sum_sum_type, Antivary.sum_mul_le_sum_mul_comp_perm, Affine.Simplex.face_centroid_eq_centroid, Fintype.prod_prod_type', NumberField.InfinitePlace.card_filter_mk_eq, prod_univ_pi, Real.volume_pi_Ioc, Fintype.expect_eq_zero_iff_of_nonneg, univ_add_of_zero_mem, univ_subset_iff, PiTensorProduct.constantBaseRingEquiv_tprod, PiLp.edist_eq_sum, Set.Sized.subset_powersetCard_univ, MeasureTheory.FiniteMeasure.pi_pi, ContinuousMultilinearMap.le_opNorm, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, Equiv.Perm.card_of_cycleType_eq_zero_iff, Finsupp.prod_zpow, RootPairing.rootForm_root_self, MeasureTheory.ProbabilityMeasure.pi_pi, add_univ_of_zero_mem, Real.volume_Icc_pi_toReal, filter_le_lt_eq_Ico, CategoryTheory.Limits.biproduct.lift_matrix_assoc, CategoryTheory.Limits.biproduct.lift_desc_assoc, Nat.multinomial_univ_two, quadraticChar_sum_zero, Affine.Simplex.sum_mongePointVSubFaceCentroidWeightsWithCircumcenter, noncommSum_single, ZMod.completedLFunction_def_odd, mem_univ_val, ContinuousAlternatingMap.le_opNorm, Matrix.trace_diagonal, MeasureTheory.volume_sum_rpow_lt, smul_univ, image_univ_of_surjective, CStarMatrix.mul_apply, Module.Basis.coe_sumCoords_of_fintype, DFinsupp.prod_eq_prod_fintype, NumberField.mixedEmbedding.convexBodySumFun_apply, filter_univ_mem, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, Matrix.IsHermitian.trace_eq_sum_eigenvalues, Algebra.SubmersivePresentation.jacobianRelations_spec, MeasureTheory.integral_fintype_iUnion, univ_val_map_subtype_val, GaussianFourier.integrable_cexp_neg_mul_sum_add, SimpleGraph.IsTuranMaximal.card_parts_le, AddSubgroup.index_pi, Fintype.not_linearIndependent_iffβ, FormalMultilinearSeries.compAlongComposition_nnnorm, NumberField.InfinitePlace.card_eq_card_isUnramifiedIn, Fintype.expect_bijective, IsAddCyclic.card_nsmul_eq_zero_le, Fintype.prod_add, AddChar.expect_apply_eq_zero_iff_ne_zero, MeasureTheory.lintegral_mul_prod_lintegral_pow_le, Fintype.prod_ite_zero, Tuple.lt_card_ge_iff_apply_ge_of_antitone, sum_subtype, Module.Basis.det_unitsSMul, MonoidHom.noncommPiCoprod_apply, TannakaDuality.FiniteGroup.sumSMulInv_apply, FiniteField.card_image_polynomial_eval, MultilinearMap.exists_bound_of_continuous, toLeft_univ, Fintype.sum_dite_eq, eq_univ_of_card, Ideal.iInf_span_singleton_natCast, Fintype.card_mul_expect, Fintype.sum_single_smul, MultilinearMap.domCoprod_alternization_coe, FiniteField.sum_subgroup_units_eq_zero, Behrend.map_apply, Pi.card_Ioc, List.sum_take_ofFn, LinearMap.IsSymmetric.diagonalization_symm_apply, ContinuousAlternatingMap.map_sum, List.toFinset_finRange, Real.volume_pi_Ioc_toReal, TensorProduct.dualDistribEquivOfBasis_symm_apply, BoxIntegral.BoxAdditiveMap.volume_apply, FunOnFinite.linearMap_apply_apply, Fintype.prod_eq_one_iff_of_le_one, SimpleGraph.Walk.IsHamiltonian.support_toFinset, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ΞΉ_app, PiLp.dist_eq_of_L1, Pi.card_Icc, Fintype.sum_ite_eq_ite_exists, univ_nonempty, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, Fin.sum_cons, cfcβ_sum_univ, Fin.prod_univ_zero, univ_eq_empty, Subgroup.noncommPiCoprod_apply, OrthonormalBasis.sum_sq_norm_inner_right, Submodule.sum_mem_iSup, MeasureTheory.Measure.pi_ball, MulAction.card_eq_sum_card_group_div_card_stabilizer', bernstein.variance, OrthonormalBasis.starProjection_eq_sum_rankOne, Orientation.abs_volumeForm_apply_of_pairwise_orthogonal, sum_conjClasses_card_eq_card, FDRep.average_char_eq_finrank_invariants, UnitsInt.univ, MvPolynomial.eval_eq', AddChar.sum_apply_eq_zero_iff_ne_zero, map_univ_equiv, Set.mem_pow_iff_prod, WittVector.wittZSMul_vars, IsPrimitiveRoot.sum_eq_zero_iff_forall_eq, Module.piEquiv_apply_apply, Equiv.Perm.sign_eq_prod_prod_Iio, Fintype.card_piFinset, Fintype.prod_ite_mem, inter_eq_univ, MulSemiringAction.charpoly_eq_prod_smul, Fintype.card_sigma, Polynomial.card_support_eq, IsAddCyclic.image_range_card, FormalMultilinearSeries.compAlongComposition_bound, AlternatingMap.exists_bound_of_continuous, OrthonormalBasis.equiv_apply, FinVec.sum_eq, prod_mul_prod_compl, Matrix.mul_apply, Matrix.Module.smul_def, extDerivWithin_apply_vectorField_of_pairwise_commute, Fintype.prod_eq_prod_compl_mul, prod_coe_sort, filter_lt_eq_Ioi, MeasureTheory.volume_sum_rpow_le, MeasureTheory.Measure.pi_map_eval, ProbabilityTheory.covariance_sum_left, Fintype.sum_ite_mem, Matrix.one_vecMul, SimpleGraph.even_card_odd_degree_vertices, MulChar.sum_one_eq_card_units, RootPairing.corootForm_apply_apply, Sum.Lex.Ici_inl, Matrix.frobenius_norm_def, DirichletCharacter.sum_char_inv_mul_char_eq, univ_map_equiv_to_embedding, MulAction.stabilizer_finset_univ, fkg, Pi.card_uIcc, Fintype.prod_prod_type, Representation.norm_ofMulDistribMulAction_eq, Iic_top, univ_product_univ, hasFDerivAt_list_prod', Fintype.sum_neg, univ_unique, PiLp.norm_eq_sum, subset_powersetCard_univ_iff, MeasureTheory.charFun_pi, univ_perm_option, Fintype.sum_congr, Matrix.toLin_self, Rep.coindToInd_apply, pi_eq_sum_univ', Fintype.balance_apply, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, MeasureTheory.Measure.pi_singleton, Fintype.prod_sum, ContinuousMultilinearMap.norm_map_init_le, CategoryTheory.Limits.biproduct.lift_desc, MeasureTheory.Integrable.fintype_prod_dep, Fin.card_filter_val_lt, Antivary.sum_smul_lt_sum_comp_perm_smul_iff, AddMonoid.exponent_pi, Affine.Simplex.sum_excenterWeightsUnnorm_singleton_pos, prod_apply_dite, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, PiToModule.fromMatrix_apply_single_one, Matrix.det_updateRow_sum, exists_sum_eq_one_iff_pairwise_coprime', CategoryTheory.rightDistributor_inv, ContinuousMultilinearMap.map_add_univ, Fin.accumulate_apply, Subgroup.mem_closure_range_iff_of_fintype, Fintype.exists_lt_card_fiber_of_mul_lt_card, Subgroup.index_iInf_le, Antivary.sum_smul_le_sum_smul_comp_perm, eq_pos_convex_span_of_mem_convexHull, iteratedDerivWithin_scomp_eq_sum_orderedFinpartition, Pi.card_Iio, EuclideanSpace.sphere_zero_eq, FGModuleCat.FGModuleCatCoevaluation_apply_one, card_nthRoots_subgroup_units, Fintype.univ_pempty, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, MeasureTheory.integral_fintype, dens_eq_one, OrthonormalBasis.sum_sq_inner_left, LinearEquiv.piRing_symm_apply, Function.minimalPeriod_piMap_fintype, Finpartition.mem_part_ofSetoid_iff_rel, NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow, CompleteOrthogonalIdempotents.option, AkraBazziRecurrence.p_def, Equiv.Perm.card_of_cycleType, Colex.ofColex_top, Fintype.exists_card_fiber_le_of_card_le_nsmul, Matrix.vandermonde_transpose_mul_vandermonde, Fin.prod_const, Fintype.prod_pi_mulSingle', tprod_fintype, toRight_univ, Polynomial.separable_prod, Matrix.toLinearMapβββ_apply, MultilinearMap.freeDFinsuppEquiv_single, Fin.Iio_last_eq_map, LineDeriv.laplacianCLM_eq_sum, MultilinearMap.map_add_sub_map_add_sub_linearDeriv, fold_sup_univ, Matrix.vecMul_eq_sum, NumberField.InfinitePlace.card_isUnramified, Fin.lt_card_filter_univ_iff_apply_of_imp, AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet, CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup, ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal, sum_embeddings_eq_finrank_mul, Fintype.prod_eq_mul_prod_compl, Fintype.prod_bool, BoxIntegral.Box.volume_face_mul, MeasureTheory.Measure.pi_univ, sum_row_of_mem_doublyStochastic, Matrix.sum_single_ofNat, Set.toFinset_eq_univ, ProbabilityTheory.covariance_fun_sum_left, NumberField.mixedEmbedding.adjust_f, hasSum_fintype, ProbabilityTheory.covariance_sum_sum, Fin.mul_prod_removeNth, RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift, Fintype.prod_pi_mulSingle, Polynomial.card_support_eq', PiTensorProduct.dualDistribInvOfBasis_apply, nilpotencyClass_pi, Fintype.univ_unit, Fin.prod_univ_castSucc, Submodule.mem_span_finset', NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, addRothNumber_le_ruzsaSzemerediNumber, AffineBasis.sum_coord_apply_eq_one, Fin.sum_univ_one, Real.volume_pi_le_prod_diam, Multiset.prod_eq_prod_coe, IsAddKleinFour.eq_finset_univ, Subfield.roots_X_pow_char_sub_X_bot, AkraBazziRecurrence.strictAnti_sumCoeffsExp, IntermediateField.coe_sum, untrop_sum, hasFDerivAt_list_prod_finRange', univ_filter_mem_range, Fintype.prod_prod_type_right', sum_compl_add_sum, Monoid.lcm_orderOf_eq_exponent, Monoid.lcm_orderOf_dvd_exponent, WittVector.mul_polyOfInterest_vars, expect_boole_mul', Fin.prod_univ_seven, Fin.sum_univ_seven, eq_affineCombination_of_mem_affineSpan_of_fintype, ProbabilityTheory.variance_fun_sum, noncommProd_mulSingle, HomogeneousLocalization.Away.span_mk_prod_pow_eq_top, univ_fin2, inv_filter_univ, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues, Antivary.sum_mul_eq_sum_mul_comp_perm_iff, ZMod.completedLFunction_eq, univ_mul_univ, Monovary.sum_comp_perm_smul_lt_sum_smul_iff, compl_filter, AddChar.sum_eq_zero_of_ne_one, Fintype.expect_one, CStarMatrix.toCLM_apply_eq_sum, NumberField.InfinitePlace.card_isUnramified_compl, Affine.Triangle.prod_dist_eq_prod_dist_of_mem_line_of_mem_line, BoxIntegral.Box.volume_apply', MeasureTheory.measureReal_iUnion_fintype, Fin.sum_univ_eight, sum_pow_of_commute, FiniteField.sum_subgroup_pow_eq_zero, Multiset.map_univ_coe, WithCStarModule.pi_norm, toLeft_eq_empty, completeOrthogonalIdempotents_iff, Multiset.map_univ_val_equiv, LinearMap.pi_apply_eq_sum_univ, Module.sum_smul_eq_zero_of_isTrivialRelation, ZMod.dft_apply, Matrix.liftLinear_apply, Pi.nnnorm_def', Fin.univ_image_get', TensorPower.multilinearMapToDual_apply_tprod, Module.Basis.mem_submodule_iff', finprod_eq_prod_of_fintype, Module.Basis.sum_dual_apply_smul_coord, univ_sigma_univ, Fintype.prod_eq_mul, Pi.sum_nnnorm_apply_le_nnnorm, IsLocalFrameOn.eventually_eq_sum_coeff_smul, Multiset.map_univ_coeEmbedding, Pi.sum_norm_apply_le_norm, Affine.Simplex.smul_faceOppositeCentroid_vsub_point_eq_sum_vsub, centroid_univ, Module.Basis.sum_repr_mul_repr, MvPolynomial.degrees_indicator, MeasureTheory.Measure.infinitePi_singleton_of_fintype, WittVector.wittAdd_vars, PiLp.norm_sq_eq_of_L2, Fintype.all_card_le_filter_rel_iff_exists_injective, Matrix.det_diagonal, MvPolynomial.evalβ_eq', compl_univ, PiLp.norm_eq_of_L1, Ici_bot, ZSpan.norm_fract_le, Fintype.card_subtype, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, SimpleGraph.extremalNumber_of_fintypeCard_eq, RCLike.wInner_const_left, Configuration.sum_lineCount_eq_sum_pointCount, RCLike.wInner_cWeight_const_left, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, Set.powersetCard.coe_finset, AlternatingGroup.card_of_cycleType, NumberField.canonicalEmbedding.nnnorm_eq, Fin.sum_univ_three, inclusion_exclusion_card_biUnion, Matrix.adjugate_diagonal, Fintype.card_filter_piFinset_eq_of_mem, AddChar.expect_eq_zero_iff_ne_zero, Affine.Simplex.inradius_eq_abs_inv_sum, Matrix.vandermonde_mul_vandermonde_transpose, mem_parallelepiped_iff, ContinuousLinearMap.norm_map_tail_le, Finsupp.univ_sum_single_apply, Fintype.sum_bool, MvPolynomial.support_esymm', Matrix.toLinearMapβββ'_apply, szemeredi_regularity, Pi.norm_def, Sum.Lex.Ioi_inl, CategoryTheory.Abelian.Ext.mkβ_sum, Matrix.sum_col_of_mem_colStochastic, toRight_eq_univ, Affine.Simplex.point_vsub_faceOppositeCentroid_eq_smul_sum_vsub, groupHomology.inhomogeneousChains.d_single, ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal, RootPairing.rootForm_apply_apply, Matrix.permanent_diagonal, Module.Basis.sum_toMatrix_smul_self, Fintype.sum_pos_iff_of_nonneg, compl_empty, Complex.volume_sum_rpow_lt, Monovary.sum_mul_comp_perm_le_sum_mul, MvPolynomial.schwartz_zippel_sup_sum, Module.Basis.reindexFinsetRange_repr_self, MeasureTheory.measure_preimage_snd_singleton_eq_sum, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, iteratedDeriv_vcomp_eq_sum_orderedFinpartition, Fintype.piFinset_of_isEmpty, Fin.sum_congr', Fintype.sum_bijective, Pi.sum_nnnorm_apply_le_nnnorm', InnerProductSpace.gramSchmidtOrthonormalBasis_det, sum_centroidWeightsIndicator_eq_one_of_card_ne_zero, OrthonormalBasis.sum_sq_norm_inner_left, Antivary.sum_smul_lt_sum_smul_comp_perm_iff, Real.volume_pi_Ioo, OrthonormalBasis.equiv_apply_euclideanSpace, RootPairing.PolarizationIn_apply, SimpleGraph.IsTuranMaximal.isEquipartition, prod_prod_Ioi_mul_eq_prod_prod_off_diag, Finsupp.sum_nsmul, Fin.univ_image_get, Nat.bell_succ, PiTensorProduct.dualDistrib_apply, Submonoid.exists_of_mem_closure_range, Fintype.exists_lt_card_fiber_of_nsmul_lt_card, Fin.prod_univ_eq_prod_range, TemperedDistribution.laplacian_eq_sum, WithCStarModule.pi_inner, AdjoinRoot.powerBasisAux'_repr_symm_apply, Fintype.existsUnique_iff_card_one, ContinuousMultilinearMap.ratio_le_opNorm, ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal, Ideal.iInf_span_singleton, Submodule.span_eq_iUnion_nat, Matrix.det_succ_column, TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially, Affine.Simplex.sum_circumcenterWeightsWithCircumcenter, CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf, map_finset_prod, Basis.multilinearMap_apply_apply, Polynomial.separable_prod_X_sub_C_iff, Set.Finite.toFinset_range, Fintype.expect_ite_mem, Pi.orderOf, Rep.standardComplex.d_of, prod_attach_univ, Fintype.exists_le_card_fiber_of_mul_le_card, SimpleGraph.dart_fst_fiber, filter_lt_lt_eq_Ioo, product_eq_univ, extDerivWithin_apply_vectorField, ZMod.LFunction_def_even, Affine.Simplex.faceOppositeCentroid_eq_sum_vsub_vadd, Real.volume_pi_Ioo_toReal, Algebra.norm_eq_prod_automorphisms, Fintype.sum_nonpos, RCLike.wInner_const_right, LinearMap.sumOfConjugates_apply, Submodule.mem_span_iff_of_fintype, EuclideanSpace.norm_eq, Subgroup.index_pi, HasFDerivWithinAt.multilinear_comp, ProbabilityTheory.iIndepFun_iff_charFunDual_pi, Matrix.mem_rowStochastic_iff_sum, stdSimplex.sum_eq_one, MultilinearMap.map_add_eq_map_add_linearDeriv_add, wittStructureInt_vars, ContinuousAlternatingMap.map_add_univ, Matrix.IsHermitian.det_eq_prod_eigenvalues, ProbabilityTheory.covarianceBilin_apply_pi, Affine.Simplex.sum_excenterWeights_eq_one_iff, sum_centroidWeightsIndicator, ProbabilityTheory.covariance_fun_sum_right, Fin.univ_succ, FormalMultilinearSeries.compAlongComposition_norm, sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one, prod_dite_of_false, OrthonormalBasis.sum_repr_symm, nndist_pi_def, HasStrictFDerivAt.continuousAlternatingMap_apply, RootPairing.CoPolarization_apply, DomMulAct.stabilizer_card', sum_hom_units_eq_zero, coe_eq_univ, Fin.add_sum_removeNth, Fin.card_filter_univ_succ', IsAddCyclic.card_addOrderOf_eq_totient, Fintype.card_eq_sum_ones, Finsupp.prod_pow, Fintype.sum_prod_type', ssubset_univ_iff, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, LieModule.traceForm_eq_sum_finrank_nsmul, Matrix.toBilin'_apply, Fintype.prod_of_injective, Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter, Fin.prod_univ_two', RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, MeasureTheory.piPremeasure_pi', Fin.prod_snoc, Tuple.lt_card_le_iff_apply_le_of_monotone, IsCyclic.image_range_card, Matrix.toLin_apply, sym2_univ, sum_range, support_finRotate, Matrix.Module.smul_apply, Fin.sum_univ_zero, Matrix.charpoly_coeff_eq_prod_coeff_of_le, MultilinearMap.freeFinsuppEquiv_apply, Module.Basis.constr_apply_fintype, Fintype.prod_dvd_of_isRelPrime, MultilinearMap.alternatization_apply, trop_iInf, Fin.image_castSucc, Equiv.prod_comp, inhomogeneousCochains.d_hom_apply, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, MvPolynomial.psum_one, Fintype.prod_dite_eq, prod_fiberwise', iSupIndep.sup_indep_univ, eq_univ_of_forall, ContinuousAlternatingMap.norm_image_sub_le', Submodule.top_le_span_range_iff_forall_exists_fun, Set.ncard_iUnion_le_of_fintype, Matrix.det_succ_column_zero, Fintype.sum_strictMono, MeasureTheory.Measure.pi_closedBall, Fin.prod_univ_two, Function.Bijective.finset_prod, Pi.card_Ico, map_univ_of_surjective, univ_eq_attach, MulSemiringAction.charpoly_eq, Subgroup.relIndex_iInf_le, Basis.mem_ideal_iff', Fintype.prod_subtype_mul_prod_subtype, exists_signed_sum', Matrix.mulVec_eq_sum, expect_boole_mul, Fintype.sum_nonneg, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, AffineBasis.toMatrix_row_sum_one, DirichletCharacter.sum_characters_eq_zero, MeasureTheory.OuterMeasure.pi_pi_le, Set.powersetCard.coe_addActionHom_of_embedding, Nat.mem_antidiagonalTuple, hasStrictFDerivAt_list_prod_attach', CategoryTheory.Limits.biproduct.total, NumberField.mixedEmbedding.convexBodyLT'_volume, Fin.univ_image_def, Function.updateFinset_univ_apply, univ_perm_fin_succ, univ_val_map_subtype_restrict, Algebra.discr_powerBasis_eq_prod, associated_norm_prod_smith, fderiv_continuousAlternatingMap_apply_apply, Module.finrank_pi_fintype, PiLp.dist_sq_eq_of_L2, Affine.Simplex.incenter_eq_affineCombination, NumberField.InfinitePlace.sum_eq_sum_add_sum, Submodule.mem_span_range_iff_exists_fun, Fin.sum_univ_def, Fintype.univ_ofIsEmpty, prod_coe_sort_eq_attach, Finpartition.ofSetoid_parts_val, Fin.prod_univ_succ, ContinuousAlternatingMap.le_of_opNorm_le, prod_attach_eq_prod_dite, Fin.prod_univ_add, Monovary.sum_comp_perm_mul_eq_sum_mul_iff, Fintype.expect_balance, CompleteOrthogonalIdempotents.iff_ortho_complete, Matrix.BlockTriangular.det, IsCyclic.card_orderOf_eq_totient, SlashInvariantForm.coe_trace, Fintype.sum_pi_single, CategoryTheory.Limits.biproduct.matrix_desc, smul_univβ', Representation.norm_ofDistribMulAction_eq, MultilinearMap.freeFinsuppEquiv_single, TannakaDuality.FiniteGroup.sumSMulInv_single_id, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt, WittVector.wittSub_vars, Affine.Simplex.eq_centroid_iff_sum_vsub_eq_zero, FormalMultilinearSeries.apply_eq_prod_smul_coeff, noncommSum_add_single, ProbabilityTheory.Kernel.iIndep.meas_iInter, LinearMap.equivariantProjection_apply, pi_eq_sum_univ, MvPolynomial.prod_X_add_C_coeff, Sum.Lex.Iio_inr, Matrix.det_blockDiagonal, Fintype.univ_Prop, Multiset.map_univ, finsum_eq_sum_of_fintype, Nat.prod_pow_primeFactors_factorization, MeasureTheory.piPremeasure_pi, Fin.sum_univ_four, sum_sum_Ioi_add_eq_sum_sum_off_diag, Fintype.sum_neg_iff_of_nonpos, Ideal.mem_span_range_iff_exists_fun, sum_ite_mem_eq, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, compl_eq_univ_iff, AlgebraicClosure.Monics.map_eq_prod, PMF.integral_eq_sum, Monoid.exponent_eq_max'_orderOf, sum_dite_of_false, fderivWithin_continuousAlternatingMap_apply_apply, piecewise_univ, Fintype.expect_equiv, Fintype.sum_eq_sum_compl_add, Fin.sum_univ_six, MeasureTheory.integral_fin_nat_prod_eq_prod, Fintype.prod_apply, MeasureTheory.charFunDual_eq_pi_iff, Function.Bijective.prod_comp, SimpleGraph.dart_card_eq_sum_degrees, MeasureTheory.volume_pi_ball, PiLp.norm_eq_of_nat, mul_univ_of_one_mem, List.prod_ofFn, WittVector.wittPow_vars, Matrix.toLinAlgEquiv_apply, Nat.card_sigma, Fintype.not_linearIndependent_iff, Monovary.sum_smul_comp_perm_lt_sum_smul_iff, QuadraticMap.weightedSumSquares_apply, Nat.prod_eq_of_mem_finMulAntidiag, IsCyclic.card_pow_eq_one_le, subset_univ_image_iff, SimpleGraph.isNClique_map_copy_top, eigenvalue_mem_ball, sum_single_ite, BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le, Fintype.sum_eq_add, SimplicialObject.Splitting.decomposition_id, NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral, EuclideanSpace.ball_zero_eq, LinearMap.sum_single_apply, inv_univ, Finsupp.univ_sum_single, smul_finset_eq_univ, Affine.Simplex.exsphere_univ, CategoryTheory.Mat.comp_apply, mulEnergy_eq_sum_sq, WithCStarModule.pi_norm_le_sum_norm, Cardinal.prod_eq_of_fintype, univ_nontrivial_iff, RCLike.wInner_one_const_right, QuadraticMap.pi_apply, Matrix.posSemidef_iff_eq_sum_vecMulVec, Matrix.toLinearMapβ_apply, MvPolynomial.hsymm_one, Matrix.charpoly_sub_diagonal_degree_lt, MultilinearMap.freeDFinsuppEquiv_apply, DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_eq, Fin.prod_trunc, centroid_eq_centroid_image_of_inj_on, CompleteOrthogonalIdempotents.complete, Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter, four_functions_theorem_univ, List.Nat.mem_antidiagonalTuple, supIndep_univ_bool, HasFDerivAt.list_prod', Fin.sum_pow_mul_eq_add_pow, Fin.sum_univ_getElem, TensorProduct.dualDistribInvOfBasis_apply, LinearMap.trace_eq_sum_trace_restrict, ProbabilityTheory.iIndepFun.integral_prod_eq_prod_integral, Affine.Simplex.exradius_eq_abs_inv_sum, MvPolynomial.aeval_esymm_eq_multiset_esymm, prod_set_coe, Monovary.sum_comp_perm_mul_lt_sum_mul_iff, filter_ge_eq_Iic, toRight_eq_empty, Set.Sized.univ_mem_iff, AddSubmonoid.mem_closure_iff_of_fintype, Mathlib.Meta.Finset.univ_eq_elems, Fintype.exists_card_fiber_lt_of_card_lt_mul, sum_toFinset_eq_subtype, Affine.Simplex.ExcenterExists.sum_excenterWeights_eq_one, card_fin, Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter, Matrix.det_updateCol_sum, univ_eq_singleton_of_card_one, Polynomial.eval_eq_sum_degreeLTEquiv, Matrix.star_dotProduct_gram_mulVec, prod_fiberwise, MvPolynomial.prod_C_add_X_eq_sum_esymm, Function.updateFinset_univ, Fin.sort_univ, MeasureTheory.measureReal_iUnion_fintype_le, ProbabilityTheory.HasGaussianLaw.fun_sum, MeasureTheory.volume_pi_closedBall, GaussianFourier.integral_cexp_neg_mul_sum_add, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', SimpleGraph.dart_fst_fiber_card_eq_degree, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, filter_subset_univ, PiTensorProduct.mapL_opNorm, Module.length_pi_of_fintype, Matrix.mem_colStochastic_iff_sum, mem_powersetCard_univ, Nat.card_pi, Real.volume_pi_Ico_toReal, Matrix.det_mul_aux, Affine.Simplex.sum_inv_height_sq_smul_vsub_eq_zero, parallelepiped_eq_sum_segment, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace, tsum_fintype, Matrix.toLinAlgEquiv_self, commProb_pi, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, Fintype.prod_ite_eq', MeasureTheory.lintegral_fintype, inclusion_exclusion_sum_biUnion, Matrix.det_mul_column, iteratedDeriv_comp_eq_sum_orderedFinpartition, ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity, mem_convexHull_iff_exists_fintype, Algebra.SubmersivePresentation.exists_sum_eq_Ο_jacobian_mul_Ο_jacobian_inv_sub_one, MonoidHom.card_fiber_eq_of_mem_range, SimpleGraph.degree_eq_sum_if_adj, PiLp.nnnorm_eq_of_L1, HasFDerivAt.linear_multilinear_comp, Pi.nnnorm_def, ContinuousMultilinearMap.le_opNorm_mul_prod_of_le, univ_mul_of_one_mem, Monovary.sum_comp_perm_smul_eq_sum_smul_iff, Monovary.sum_comp_perm_smul_le_sum_smul, FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1, CategoryTheory.Limits.biproduct.lift_matrix, IsCompl.prod_mul_prod, Multiset.prod_toEnumFinset, FiniteField.sum_pow_units, support_finRotate_of_le, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, Affine.Simplex.centroid_eq_affineCombination, expect_univ, Fintype.exists_disjointed_le, Polynomial.sum_fin, ProbabilityTheory.iIndepFun_iff_charFun_pi, MvPolynomial.degrees_esymm, WittVector.polyOfInterest_vars, MvPolynomial.esymm_eq_sum_monomial, AddEquiv.finsuppUnique_symm_apply_support_val, ContinuousMultilinearMap.opNNNorm_le_iff, Fintype.sum_smul_sum, Affine.Simplex.affineCombination_touchpointWeights, Set.toFinset_iUnion, CategoryTheory.Limits.biproduct.desc_eq, det_fderivPiPolarCoordSymm, Module.finrank_directSum, univ_add_univ, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, Multiset.map_univ_comp_coe, piecewise_erase_univ, Matrix.sum_single_intCast, univ_shatters, noncommProd_mul_single, dist_pi_def, univ_sub_univ, Fintype.prod_lt_one, AddAction.sum_card_fixedBy_eq_card_orbits_mul_card_addGroup, AddSubmonoid.mem_closure_range_iff_of_fintype, ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply, ProbabilityTheory.iIndepFun.meas_iInter, IsAddUnit.sum_univ_iff, prod_dite, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod, Matrix.IsHermitian.roots_charpoly_eq_eigenvaluesβ, MeasureTheory.charFunDual_eq_pi_iff', MultilinearMap.alternatization_coe, ModularForm.coe_norm, Fin.prod_Ioi_zero, map_orderEmbOfFin_univ, Affine.Simplex.smul_centroid_vsub_point_eq_sum_vsub, finPiFinEquiv_single, ContinuousMultilinearMap.bound, CategoryTheory.Mat_.comp_apply, Antivary.sum_mul_lt_sum_comp_perm_mul_iff, Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, List.prod_take_ofFn, OrthogonalFamily.sum_projection_of_mem_iSup, LinearMap.IsSymmetric.trace_eq_sum_eigenvalues, SimpleGraph.IsTuranMaximal.card_parts, ContinuousAlternatingMap.opNorm_le_iff, prod_finset_coe, mem_fintypeAffineCoords_iff_sum, Affine.Simplex.sum_touchpointWeights, Fintype.sum_fiberwise, Affine.Simplex.sum_pointWeightsWithCircumcenter, Algebra.algebraMap_intNorm_of_isGalois, univ_inter, attach_affineCombination_of_injective, prod_ite_mem_eq, Finsupp.prod_fintype, MvPolynomial.sum_eval_eq_zero, VectorFourier.fourierPowSMulRight_apply, extDeriv_apply_vectorField_of_pairwise_commute, Module.Basis.repr_sum_self, MvPolynomial.msymm_one, CategoryTheory.Mat.comp_def, AddMonoid.lcm_addOrderOf_eq_exponent, EuclideanSpace.dist_eq, Set.mem_fintype_sum, Set.toFinset_univ, Fintype.prod_bijective, SchwartzMap.laplacian_eq_sum, stdSimplex.barycenter_eq_centerMass, Set.encard_pi_eq_prod_encard, OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, ContinuousMultilinearMap.le_of_opNorm_le, Fin.map_valEmbedding_univ, univ_option, Fintype.prod_unique, AlgebraicTopology.DoldKan.Nβ_obj_X_d, ModularForm.prod_fintype_slash, GaussianFourier.integral_cexp_neg_sum_mul_add, jacobiSum_eq_sum_sdiff, Fintype.prod_boole, RCLike.wInner_one_const_left, fderivWithin_list_prod', Fintype.prod_subsingleton, sum_mem_multiset, prod_range, Affine.Simplex.ExcenterExists.signedInfDist_excenter, Orientation.volumeForm_apply_le, endVecAlgEquivMatrixEnd_symm_apply_apply, MeasureTheory.Measure.mkMetric_le_liminf_sum, edist_pi_def, CategoryTheory.Limits.biproduct.lift_eq, BoxIntegral.Box.volume_apply, QuadraticMap.Ring.associated_pi, ProbabilityTheory.iIndepFun.hasGaussianLaw_sum, prod_congr_set, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, trace_eq_sum_embeddings, catalan_succ, MvPolynomial.esymm_eq_multiset_esymm, Matrix.det_mul_row, CompleteOrthogonalIdempotents.prod_one_sub, Monovary.sum_mul_comp_perm_lt_sum_mul_iff, Submonoid.mem_closure_range_iff_of_fintype, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace, FDRep.char_orthonormal, OrthonormalBasis.sum_repr, Fintype.sum_balance, Polynomial.sum_modByMonic_coeff, MvPolynomial.support_esymm'', Antivary.sum_smul_comp_perm_eq_sum_smul_iff, PiTensorProduct.ofFinsuppEquiv'_apply_apply, Fintype.prod_ite_eq_ite_exists, MeasureTheory.measure_iUnion_fintype_le, PiLp.dist_eq_of_L2, Submodule.mem_span_set', FunOnFinite.map_apply_apply, finSigmaFinEquiv_one, Antivary.card_mul_sum_le_sum_mul_sum, NumberField.InfinitePlace.prod_eq_prod_mul_prod, SzemerediRegularity.coe_m_add_one_pos, MeasureTheory.Integrable.fintype_prod, sum_univ_pi, LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum, ZMod.invDFT_def, OrthonormalBasis.sum_rankOne_eq_id, Fintype.sum_sigma', Matrix.sum_single_natCast, Antivary.card_smul_sum_le_sum_smul_sum, coe_filter_univ, filter_lt_le_eq_Ioc, Fin.sum_univ_succAbove, Module.Basis.orientation_unitsSMul, MeasureTheory.integral_fintype_prod_volume_eq_prod, Affine.Simplex.sum_pointsWithCircumcenter, Fintype.sum_mul_sum, Fintype.univ_bool, Algebra.discr_powerBasis_eq_prod'', vadd_univ, CategoryTheory.leftDistributor_inv, Set.toFinset_ssubset_univ, centroid_pair_fin, Submodule.finrank_quotient_eq_sum, Matrix.trace_blockDiagonal, sum_apply_dite, Fin.prod_univ_six, Nonempty.eq_univ, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, OrthonormalBasis.coe_equiv_euclideanSpace, RCLike.wInner_one_eq_sum, ProbabilityTheory.Kernel.iIndepFun.meas_iInter, MvPolynomial.IsHomogeneous.sum_X_mul_pderiv, Matrix.sum_single_eq_diagonal, EuclideanSpace.dist_sq_eq, AkraBazziRecurrence.h_rec, sum_attach_univ, prod_mem_multiset, LieModule.traceForm_eq_sum_finrank_nsmul_mul, ProbabilityTheory.iIndepFun.integral_fun_prod_eq_prod_integral, AddSubgroup.mem_closure_iff_of_fintype, inter_univ, Matrix.det_of_upperTriangular, Fintype.prod_congr, NumberField.Units.exist_unique_eq_mul_prod, Fin.univ_castSuccEmb, Complex.lintegral_comp_pi_polarCoord_symm, NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image, Matrix.represents_iff', Submonoid.mem_closure_finset', Finsupp.coe_univ_sum_single, PiLp.nnnorm_eq_sum, Fintype.prod_Prop, WittVector.wittNSMul_vars, Fintype.prod_sumElim, nsmul_univ, ProbabilityTheory.iIndep.meas_iInter, Affine.Simplex.sum_excenterWeightsUnnorm_empty_pos, Fin.prod_insertNth, ContinuousMultilinearMap.norm_map_insertNth_le, Fintype.prod_ite_eq, Fintype.sum_subset, Fintype.univ_punit, fderivWithin_continuousAlternatingMap_apply, Equiv.Perm.sign_prodCongrRight, GaussianFourier.integrable_cexp_neg_sum_mul_add, finsetCongr_piAntidiag_eq_antidiag, iteratedDerivWithin_comp_eq_sum_orderedFinpartition, Fin.prod_univ_def, Matrix.frobenius_nnnorm_def, WithCStarModule.pi_norm_sq, NumberField.mixedEmbedding.fundamentalCone.sum_eq_zero_of_mem_span_completeFamily, Set.Finite.convexHull_eq_image, Algebra.discr_powerBasis_eq_prod', Affine.Triangle.prod_div_one_sub_eq_one_of_mem_line_point_lineMap, SimpleGraph.edgeSet_univ_card, sum_fiberwise, AlternatingMap.uncurryFin_apply, MvPolynomial.schwartz_zippel_sum_degreeOf, MeasureTheory.charFunDual_pi, fromModuleCatToModuleCatLinearEquiv_apply, SimplexCategory.coe_toTopMap, Fintype.linearCombination_apply, SimpleGraph.neighborFinset_eq_filter, iteratedDerivWithin_vcomp_eq_sum_orderedFinpartition, CategoryTheory.rightDistributor_hom, MultilinearMap.linearDeriv_apply, RCLike.wInner_cWeight_const_right, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer, sum_dite_of_true, Fin.sum_univ_five, MeasureTheory.addContent_iUnion, AffineBasis.centroid_mem_interior_convexHull, MultilinearMap.mkPiRing_apply, trace_eq_sum_automorphisms, Fintype.expect_ite_eq', finFunctionFinEquiv_apply_val, MultilinearMap.map_smul_univ, Finsupp.equivFunOnFinite_symm_sum, Complex.volume_sum_rpow_lt_one, AffineBasis.affineCombination_coord_eq_self, Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, Fintype.sum_prod_type_right, inf_univ_eq_iInf, EuclideanSpace.nnnorm_eq, Fintype.prod_eq_one_iff_of_one_le, PiLp.inner_apply, bernstein.probability, AkraBazziRecurrence.one_mem_range_sumCoeffsExp, ZMod.LFunction_residue_one, ProbabilityTheory.iIndepFun.integral_fun_prod_comp, SimpleGraph.sum_incMatrix_apply_of_notMem_edgeSet, sum_congr_set, Multiset.sum_eq_sum_coe, Affine.Simplex.sum_excenterWeights, Fintype.sum_extend_by_zero, NumberField.prod_archAbsVal_eq, iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, DomMulAct.stabilizer_ncard, hasStrictFDerivAt_list_prod', ContinuousMultilinearMap.opNorm_le_iff, LinearMap.IsSymmetric.re_trace_eq_sum_eigenvalues, ProbabilityTheory.iIndepFun.integral_prod_comp, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, Fintype.exists_le_card_fiber_of_nsmul_le_card, AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer', extDerivWithin_apply, iSupIndep_iff_supIndep_univ, univ_nonempty_iff, Fintype.sum_pow_mul_eq_add_pow, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_pt, val_univ_fin, ContinuousAlternatingMap.opNNNorm_le_iff, Affine.Simplex.exradius_univ, IsUnit.prod_univ_iff, MeasureTheory.GridLines.T_univ, sup_univ_eq_iSup, AlgebraicTopology.DoldKan.decomposition_Q, RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos, TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero, Matrix.det_apply', ContinuousMultilinearMap.norm_map_cons_le, FiniteField.sum_subgroup_units, AkraBazziRecurrence.continuous_sumCoeffsExp, Antivary.sum_smul_le_sum_comp_perm_smul, ContinuousAlternatingMap.bound, Subgroup.exists_of_mem_closure_range, prod_univ_sum, univ_map_embedding, Fintype.card_smul_expect, Fin.sum_const, Encodable.sortedUniv_toFinset, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card, Module.Basis.det_unitsSMul_self, SimpleGraph.copyCount_eq_card_image_copyToSubgraph, Fintype.exists_card_fiber_le_of_card_le_mul, MvPolynomial.esymm_eq_sum_subtype, Fintype.prod_dvd_of_coprime, prod_subtype, Set.encard_iUnion_le_of_fintype, ContinuousAlternatingMap.map_smul_univ, Fintype.sum_subsingleton, Fin.sum_univ_fun_getElem, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, Fintype.prod_dite_eq', Fin.sum_univ_two, Fintype.sum_equiv, bernoulli'_def', sum_set_coe, filter_gt_eq_Iio, image_subtype_ne_univ_eq_image_erase, Fintype.prod_strictMono', NumberField.InfinitePlace.prod_eq_abs_norm, PiTensorProduct.injectiveSeminorm_tprod_le, parallelepiped_eq_convexHull, sum_card_addOrderOf_eq_card_nsmul_eq_zero, Antivary.sum_comp_perm_mul_eq_sum_mul_iff, Fintype.prod_sum_type, exists_signed_sum, Equiv.Perm.sign_prodCongrLeft, Fin.Ioi_zero_eq_map, Matrix.IsHermitian.charpoly_eq, Fintype.prod_empty, NumberField.mulHeightβ_eq, AffineBasis.linear_combination_coord_eq_self, TorusIntegrable.function_integrable, NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral, sum_coe_sort_eq_attach, AddMonoid.lcm_addOrderOf_dvd_exponent, Basis.piTensorProduct_repr_tprod_apply, Fintype.nodup_map_univ_iff_injective, Fin.sum_Ioi_zero, MeasureTheory.integral_count, NumberField.Units.sum_mult_mul_log, Fintype.sum_eq_add_sum_compl, Equiv.Perm.card_of_cycleType_singleton, MvPolynomial.esymm_one, Module.Basis.sum_equivFun, Set.biUnion_finsetSigma_univ', Polynomial.degree_sum_fin_lt, iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod, PiLp.norm_eq_of_L2, Matrix.linfty_opNNNorm_replicateRow, ModularForm.coe_trace, IsLocalFrameOn.coeff_sum_eq, Fintype.prod_le_one, CategoryTheory.Mat_.comp_def, AddSubmonoid.mem_closure_finset', Multiset.count_univ, Fin.image_succAbove_univ, CategoryTheory.Limits.biproduct.map_eq, Matrix.det_succ_row_zero, Finsupp.equivFunOnFinite_symm_eq_sum, AlternatingGroup.map_subtype_of_cycleType, prod_le_univ_prod_of_one_le', prod_compl_mul_prod, trace_eq_sum_embeddings_gen, powerset_univ, Fintype.sum_apply, Set.Finite.toFinset_univ, Fintype.sum_fiberwise', neg_univ, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, smul_prod_perm, ZLattice.sum_piFinset_Icc_rpow_le, AlternatingMap.domCoprod_apply, Fintype.sum_subtype_add_sum_subtype, FDRep.scalar_product_char_eq_finrank_equivariant, Matrix.Module.smul_def', fold_inf_univ, Matrix.BlockTriangular.det_fintype, Set.image_fintype_sum_pi, QuadraticMap.Ring.polar_pi, prod_toFinset_eq_subtype, Nat.Partition.coeff_genFun, sum_finset_coe, Fintype.univ_ofSubsingleton, ContinuousMultilinearMap.le_opNNNorm, MeasureTheory.Measure.pi_pi, matrixEquivTensor_apply, ContinuousMultilinearMap.norm_compContinuousLinearMapL_le, AkraBazziRecurrence.injective_sumCoeffsExp, RootPairing.CoPolarizationIn_apply, AddChar.expect_apply_eq_ite, Matrix.charpoly_diagonal, sum_prod_piFinset, Fintype.exists_card_fiber_lt_of_card_lt_nsmul, Equiv.Perm.ofSign_disjUnion, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_Ο_app, CStarAlgebra.exists_sum_four_unitary, Algebra.norm_eq_prod_embeddings_gen, OrthonormalBasis.sum_repr', exteriorPower.toTensorPower_apply_ΞΉMulti, MvPolynomial.support_esymm, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod, subtype_univ, Fintype.sum_prod_type, finFunctionFinEquiv_apply, Fintype.prod_lt_one_iff_of_le_one, expect_pow, MeasureTheory.integral_iUnion_fintype, Fintype.sum_sumElim, Affine.Triangle.orthocenter_vsub_circumcenter_eq_sum_vsub, sup'_univ_eq_ciSup, fderiv_list_prod', ZMod.LFunction_dft, IsPrimitiveRoot.sum_eq_zero_iff_forall_eq_int, Orthonormal.inner_right_fintype, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite, AkraBazziRecurrence.sumCoeffsExp_p_eq_one, Fintype.sum_sigma, ENNReal.tsum_iUnion_le, EuclideanSpace.edist_eq, Fintype.prod_subset, Module.Basis.sum_repr, DomMulAct.stabilizer_card, Function.Odd.sum_eq_zero, Fin.card_filter_univ_eq_vector_get_eq_count, Nat.coprime_fintype_prod_right_iff, Fintype.one_lt_prod, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum, sum_card_orderOf_eq_card_pow_eq_one, WittVector.wittNeg_vars, MeasureTheory.charFun_eq_pi_iff, Affine.Simplex.excenter_univ, Fin.prod_univ_three, Equiv.Perm.support_subtypePerm, Fintype.sum_eq_zero_iff_of_nonneg, Algebra.prod_embeddings_eq_finrank_pow, Matrix.mulVec_one, sum_coe_sort, Affine.Simplex.circumcenter_eq_centroid, HasStrictFDerivAt.continuousMultilinearMap_apply, card_univ_diff, TensorProduct.exists_sum_tmul_eq, ProbabilityTheory.Kernel.iIndepSets.meas_iInter, AddSubgroup.relIndex_iInf_le, ContinuousMultilinearMap.norm_compContinuousLinearMap_le, Fin.prod_prod_eq_prod_triangle_mul, ProbabilityTheory.HasGaussianLaw.sum, one_dotProduct, Fin.sum_insertNth, Antivary.sum_mul_lt_sum_mul_comp_perm_iff, sum_add_sum_compl, PiLp.edist_eq_of_L1, MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot, sum_pow', Set.toFinset_setOf, ZMod.dft_def, univ_of_card_le_two, Set.powersetCard.coe_mulActionHom_of_embedding, Rep.barComplex.d_single, univ_filter_card_eq, addEnergy_univ_right, ContinuousLinearMap.norm_map_removeNth_le, dotProduct_one, sum_mulVec_of_mem_doublyStochastic, ContinuousMultilinearMap.norm_image_sub_le', Matrix.linfty_opNNNorm_def, MulChar.sum_eq_zero_of_ne_one, smul_univβ, Monovary.sum_smul_sum_le_card_smul_sum, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, Fintype.sum_of_injective, QuadraticMap.basisRepr_apply, Fin.prod_cons, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, exists_eq_sum_perm_of_mem_doublyStochastic, hasFDerivAt_list_prod_attach', integral_comp_pi_polarCoord_symm, AlternatingGroup.card_of_cycleType_mul_eq, SignType.univ_eq, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Nat.finMulAntidiag_eq_piFinset_divisors_filter, OrthogonalFamily.inner_right_fintype, dens_univ, WittVector.wittPolyProd_vars, Pi.card_Ioo, Pi.card_Ioi, SlashInvariantForm.coe_norm, TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective, Fintype.prod_eq_single, sum_translate, OrderedFinpartition.sum_sigma_eq_sum, MeasureTheory.volume_sum_rpow_lt_one, Matrix.BlockTriangular.charpoly, subset_univ, univ_div_univ, FiniteField.prod_univ_units_id_eq_neg_one, ContinuousAlternatingMap.alternatizeUncurryFin_apply, univ_eq_empty_iff, Fintype.sum_prod_type_right', Nat.multinomial_univ_three, CStarAlgebra.exists_sum_four_nonneg, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum, PiLp.nndist_eq_of_L2, filter_le_eq_Ici, Fintype.prod_eq_mul_prod_subtype_ne, sum_eq_sum_extend, AddChar.expect_eq_ite, MeasureTheory.measure_preimage_fst_singleton_eq_sum, ContinuousAlternatingMap.ratio_le_opNorm, stdSimplex_eq_inter, Polynomial.card_mahlerMeasure_le_prod, Matrix.linfty_opNorm_def, Fin.sum_univ_succ, NumberField.house_eq_sup', exists_mem_doublyStochastic_eq_smul_iff, compl_eq_empty_iff, PiLp.dist_eq_sum, NumberField.mixedEmbedding.convexBodySum_mem, univ_nontrivial, Turing.PartrecToTM2.supports_biUnion, PiLp.edist_eq_of_L2, Affine.Simplex.centroid_vsub_eq, ProbabilityTheory.variance_sum, MultilinearMap.alternatization_def, IsKleinFour.eq_finset_univ, Matrix.norm_eq_sup_sup_nnnorm, univ_map_subtype, extDeriv_apply, Matrix.sum_mulVec_of_mem_colStochastic, mem_finAntidiagonal, FDRep.simple_iff_char_is_norm_one, WittVector.wittPolyProdRemainder_vars, Behrend.sum_eq, Subgroup.mem_closure_iff_of_fintype, Fintype.expect_const, sum_dite, PMF.toMeasure_apply_fintype, Set.biInter_finsetSigma_univ', NumberField.mixedEmbedding.norm_apply, ZMod.dft_apply_zero, Matrix.sum_row_of_mem_rowStochastic, sum_le_univ_sum_of_nonneg, MeasureTheory.FiniteMeasure.mass_pi, Set.image_fintype_prod_pi, ContinuousAlternatingMap.le_of_opNNNorm_le, Antivary.sum_comp_perm_smul_eq_sum_smul_iff, Fintype.prod_fiberwise, compls_univ, Fin.univ_val_map, PiLp.nndist_eq_of_L1, bernsteinApproximation.apply, Set.Finite.toFinset_eq_univ, TensorPower.pairingDual_tprod_tprod, Affine.Simplex.sum_centroidWeightsWithCircumcenter, ContinuousAlternatingMap.le_opNorm_mul_prod_of_le, card_linearIndependent, nsmul_piAntidiag_univ, WittVector.wittMul_vars, MultilinearMap.map_add_univ, univ_pow, List.alternatingSum_eq_finset_sum, PMF.toOuterMeasure_apply_fintype, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, HasFDerivWithinAt.list_prod', HasFDerivAt.continuousMultilinearMap_apply, prod_dite_of_true, Fintype.sum_eq_single, prod_galRestrict_eq_norm, sum_conjneg, Monovary.sum_smul_comp_perm_eq_sum_smul_iff, Fintype.sum_Prop, shatters_univ, powerset_eq_univ, Fintype.sum_pi_single', NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm, Orientation.abs_volumeForm_apply_le, Fintype.expect_eq_sum_div_card, ProbabilityTheory.covariance_fun_sum_fun_sum
|