Commit 2023-07-02 10:21 03fc68aa

View on Github →

fix: ∑' precedence (#5615)

  • Also remove most superfluous parentheses around big operators (∑, ∏ and variants).
  • roughly the used regex: ([^a-zA-Zα-ωΑ-Ω'𝓝ℳ₀𝕂ₛ)]) \(([∑∏][^()∑∏]*,[^()∑∏:]*)\) ([⊂⊆=<≤]) replaced by $1 $2 $3

Estimated changes

modified theorem Finset.prod_attach
modified theorem Finset.prod_coe_sort
modified theorem Finset.prod_cons
modified theorem Finset.prod_const
modified theorem Finset.prod_div_distrib
modified theorem Finset.prod_empty
modified theorem Finset.prod_eq_one
modified theorem Finset.prod_eq_pow_card
modified theorem Finset.prod_eq_zero
modified theorem Finset.prod_eq_zero_iff
modified theorem Finset.prod_insert
modified theorem Finset.prod_insert_one
modified theorem Finset.prod_mul_distrib
modified theorem Finset.prod_ne_zero_iff
modified theorem Finset.prod_of_empty
modified theorem Finset.prod_pow
modified theorem Finset.prod_range_one
modified theorem Finset.prod_range_zero
modified theorem Finset.prod_singleton
modified theorem Finset.prod_zpow
modified theorem Fin.prod_const
modified theorem Fin.prod_univ_four
modified theorem Fin.prod_univ_one
modified theorem Fin.prod_univ_three
modified theorem Fin.prod_univ_two
modified theorem Fin.prod_univ_zero
modified theorem Fin.sum_const
modified theorem finprod_eq_if
modified theorem finprod_eq_prod_of_fintype
modified theorem finprod_false
modified theorem finprod_mem_def
modified theorem finprod_mem_finset_eq_prod
modified theorem finprod_mem_insert_one
modified theorem finprod_mem_mulSupport
modified theorem finprod_mem_of_eqOn_one
modified theorem finprod_mem_range
modified theorem finprod_mem_univ
modified theorem finprod_of_isEmpty
modified theorem finprod_true
modified theorem finprod_unique
modified theorem Finset.sum_range_id
modified theorem Finset.prod_eq_one_iff'
modified theorem Finset.prod_le_one'
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 geom_sum_one
modified theorem geom_sum_two
modified theorem geom_sum_zero
modified theorem one_geom_sum
modified theorem zero_geom_sum
modified theorem stdSimplex_eq_inter
modified theorem Convex.sum_mem
modified theorem Finset.centerMass_insert
modified theorem ConvexOn.map_sum_le
modified theorem Pi.sum_norm_apply_le_norm'
modified theorem memℓp_gen'
modified theorem ENNReal.tsum_geometric
modified theorem tsum_geometric_nNReal
modified theorem tsum_geometric_of_lt_1
modified theorem tsum_geometric_two'
modified theorem tsum_geometric_of_abs_lt_1
modified theorem tsum_geometric_of_norm_lt_1
modified theorem Composition.sum_blocksFun
modified theorem Real.sum_le_exp_of_nonneg
modified theorem Fintype.prod_bool
modified theorem Fintype.prod_congr
modified theorem Fintype.prod_eq_one
modified theorem Fintype.prod_eq_single
modified theorem Fintype.prod_option
modified theorem Rat.cast_prod
modified theorem Rat.cast_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 weightedVSub_mem_vectorSpan
modified theorem Basis.sum_equivFun
modified theorem Basis.sum_repr
modified theorem Finpartition.sum_card_parts
modified theorem Pmf.tsum_coe
modified theorem Pmf.tsum_coe_ne_top
modified def Pmf.ofFinset
modified def Pmf.ofFintype
modified theorem sum_hom_units_eq_zero
modified theorem Equiv.tsum_eq
modified theorem HasSum.tsum_eq
modified theorem Summable.hasSum_iff
modified theorem tsum_bool
modified theorem tsum_const_smul
modified theorem tsum_empty
modified theorem tsum_fintype
modified theorem tsum_neg
modified theorem tsum_op
modified theorem tsum_pi_single
modified theorem tsum_singleton
modified theorem tsum_subtype
modified theorem tsum_univ
modified theorem tsum_unop
modified theorem tsum_zero'
modified theorem tsum_zero
modified theorem tsum_smul_const
modified theorem hasSum_le_of_sum_le
modified theorem tsum_eq_zero_iff
modified theorem tsum_le_of_sum_le'
modified theorem tsum_le_of_sum_le
modified theorem tsum_le_of_sum_range_le
modified theorem tsum_mono
modified theorem tsum_ne_zero_iff
modified theorem tsum_nonpos
modified theorem Summable.tsum_mul_left
modified theorem Summable.tsum_mul_right
modified theorem tsum_div_const
modified theorem tsum_mul_left
modified theorem tsum_mul_right
modified theorem ENNReal.hasSum_toReal
modified theorem ENNReal.summable_toReal
modified theorem ENNReal.tendsto_sum_nat_add
modified theorem ENNReal.tsum_add_one_eq_top
modified theorem ENNReal.tsum_sub
modified theorem NNReal.tsum_strict_mono
modified theorem PartitionOfUnity.sum_eq_one
modified theorem PartitionOfUnity.sum_le_one