Commit 2024-04-30 14:24 001604ae

View on Github →

feat: ∑ x ∈ s, f x to replace ∑ x in s, f x in the future (#6795) Adds new syntax for sum/product big operators for ∑ x ∈ s, f x. The set s can either be a Finset or a Set with a Fintype instance, in which case it is equivalent to ∑ x ∈ s.toFinset, f x. Also supports ∑ (x ∈ s) (y ∈ t), f x y for Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y). Note that these are not dependent products at the moment. Adds with clauses, so for example ∑ (x ∈ Finset.range 5) (y ∈ Finset.range 5) with x < y, x * y, which inserts a Finset.filter over the domain set. Supports pattern matching in the variable position. This is by creating an experimental version of extBinder that uses term:max instead of binderIdent. The new ∑ x ∈ s, f x notation is used in Algebra.BigOperators.Basic for illustration, but the old ∑ x in s, f x still works for backwards compatibility. Zulip threads here and here

Estimated changes

modified theorem Finset.dvd_prod_of_mem
modified theorem Finset.pow_card_mul_prod
modified theorem Finset.pow_eq_prod_const
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_const_one
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_finset_coe
modified theorem Finset.prod_insert
modified theorem Finset.prod_insert_one
modified theorem Finset.prod_inv_distrib
modified theorem Finset.prod_map_val
modified theorem Finset.prod_mul_distrib
modified theorem Finset.prod_mul_pow_card
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_set_coe
modified theorem Finset.prod_singleton
modified theorem Finset.prod_zpow
modified theorem ofAdd_sum
modified theorem ofMul_prod