Commit 2024-05-27 08:32 6524156d

View on Github →

chore: Use the new ∑ i ∈ s, f i notation (#13209) Replace ∑ i in s, f i/∏ i in s, f i by ∑ i ∈ s, f i/∏ i ∈ s, f i everywhere. The former is deprecated notation that will be removed in a few months.

Estimated changes

modified theorem Imo1987Q1.main
modified theorem Imo1987Q1.main_fintype
modified theorem Imo1987Q1.main₀
modified theorem Theorems100.card_le_mul_sum
modified theorem Finset.card_eq_sum_ones
modified theorem finprod_mem_finset_eq_prod
modified theorem Finset.sum_apply'
modified theorem Finsupp.sum_sum_index'
modified theorem Finset.prod_Ico_div_bot
modified theorem Finset.sum_range_id
modified theorem Finset.sum_range_id_mul_two
modified theorem Prod.fst_prod
modified theorem Prod.snd_prod
modified theorem Finset.dvd_sum
modified theorem Finset.prod_natCast
modified theorem Fintype.prod_add
modified theorem WithBot.bot_lt_sum_iff
modified theorem WithBot.sum_eq_bot_iff
modified theorem WithBot.sum_lt_bot
modified theorem WithTop.sum_eq_top_iff
modified theorem WithTop.sum_lt_top
modified theorem WithTop.sum_lt_top_iff
modified theorem CharTwo.sum_sq
modified theorem Nat.geomSum_lt
modified theorem Odd.geom_sum_pos
modified theorem geom_sum_mul
modified theorem geom_sum_one
modified theorem geom_sum_two
modified theorem geom_sum_zero
modified theorem mul_geom_sum
modified theorem mul_neg_geom_sum
modified theorem one_geom_sum
modified theorem op_geom_sum
modified theorem op_geom_sum₂
modified theorem zero_geom_sum
modified theorem Finset.cast_card
modified theorem Submodule.coe_sum
modified theorem MvPolynomial.as_sum
modified theorem Finset.one_le_prod''
modified theorem Finset.one_le_prod'
modified theorem Finset.one_lt_prod'
modified theorem Finset.one_lt_prod
modified theorem Finset.prod_eq_one_iff'
modified theorem Finset.prod_le_one'
modified theorem Finset.prod_le_prod'
modified theorem Finset.prod_lt_one'
modified theorem Finset.prod_lt_one
modified theorem Finset.prod_mono_set'
modified theorem Finset.single_le_prod'
modified theorem Finset.prod_le_one
modified theorem Finset.prod_nonneg
modified theorem Finset.prod_pos
modified theorem IsCauSeq.of_abv
modified theorem cauchy_product
modified theorem sq_sum_le_card_mul_sum_sq
modified theorem Polynomial.coeff_zero_prod
modified theorem Polynomial.degree_prod
modified theorem Polynomial.degree_prod_le
modified theorem Polynomial.natDegree_prod'
modified theorem Polynomial.as_sum_range
modified theorem Polynomial.as_sum_support
modified theorem Asymptotics.IsBigO.sum
modified theorem Asymptotics.IsLittleO.sum
modified theorem Complex.abel_aux
modified theorem Convex.sum_mem
modified theorem Finset.centerMass_insert
modified theorem ConvexOn.map_sum_le
modified theorem nnnorm_prod
modified theorem norm_prod
modified theorem nnnorm_prod_le
modified theorem norm_prod_le
modified theorem NormedSpace.exp_sum
modified theorem memℓp_gen'
modified theorem sum_Ioo_inv_sq_le
modified theorem Seminorm.finset_sup_le_sum
modified def Complex.logTaylor
modified theorem sum_geometric_two_le
modified theorem exists_norm_le_of_cauchySeq
modified theorem norm_sum_neg_one_pow_le
modified theorem Complex.im_sum
modified theorem Complex.ofReal_prod
modified theorem Complex.ofReal_sum
modified theorem Complex.re_sum
modified theorem Complex.isCauSeq_exp
modified theorem Real.sum_le_exp_of_nonneg
modified theorem DFinsupp.card_Icc
modified theorem DFinsupp.card_Ico
modified theorem DFinsupp.card_Iic
modified theorem DFinsupp.card_Iio
modified theorem DFinsupp.card_Ioc
modified theorem DFinsupp.card_Ioo
modified theorem DFinsupp.card_uIcc
modified theorem ENNReal.coe_finset_prod
modified theorem ENNReal.coe_finset_sum
modified theorem ENNReal.prod_lt_top
modified theorem ENNReal.sum_eq_top_iff
modified theorem ENNReal.sum_lt_top
modified theorem ENNReal.sum_lt_top_iff
modified theorem Finset.sum_card_slice
modified theorem Finsupp.card_Icc
modified theorem Finsupp.card_Ico
modified theorem Finsupp.card_Iic
modified theorem Finsupp.card_Iio
modified theorem Finsupp.card_Ioc
modified theorem Finsupp.card_Ioo
modified theorem Multiset.card_Iic
modified theorem NNRat.coe_prod
modified theorem NNRat.coe_sum
modified theorem Nat.multinomial_spec
modified theorem Nat.sum_Icc_choose
modified theorem Nat.sum_range_choose
modified theorem Nat.prod_factorial_pos
modified theorem Nat.prod_Icc_factorial
modified theorem Nat.prod_primeFactors_dvd
modified theorem Nat.fib_succ_eq_succ_sum
modified theorem Nat.primeFactors_prod
modified theorem Nat.sum_totient'
modified theorem Rat.cast_prod
modified theorem Rat.cast_sum
modified theorem NNReal.coe_prod
modified theorem NNReal.coe_sum
modified def birkhoffSum
modified theorem smooth_finset_prod'
modified theorem weightedVSub_mem_vectorSpan
modified theorem Lagrange.eval_nodal
modified theorem Lagrange.nodal_eq
modified theorem sum_bernoulli'
modified theorem Nat.sum_properDivisors_dvd
modified def harmonic
modified theorem harmonic_eq_sum_Icc
modified theorem ZMod.prod_Ico_one_prime
modified theorem Finpartition.sum_card_parts
modified theorem PMF.toMeasure_apply_finset
modified def PMF.ofFinset
modified theorem IsCoprime.of_prod_left
modified theorem IsCoprime.of_prod_right
modified theorem IsCoprime.prod_left
modified theorem IsCoprime.prod_left_iff
modified theorem IsCoprime.prod_right
modified theorem IsCoprime.prod_right_iff
modified theorem IsRelPrime.of_prod_left
modified theorem IsRelPrime.of_prod_right
modified theorem IsRelPrime.prod_left
modified theorem IsRelPrime.prod_left_iff
modified theorem IsRelPrime.prod_right
modified theorem IsRelPrime.prod_right_iff
modified def MvPolynomial.degree
modified theorem Polynomial.monic_geom_sum_X
modified theorem bernsteinPolynomial.sum
modified theorem hasProd_le_of_prod_le
modified theorem isLUB_hasProd'
modified theorem le_hasProd_of_le_prod
modified theorem tprod_le_of_prod_le'
modified theorem tprod_le_of_prod_le
modified theorem tprod_le_of_prod_range_le