Namespace Finsupp 4 theorems
- Effective ℤ-divisor pushing forward to a reduced sum
Finsupp.exists_eq_sum_single_of_mapDomain_eq_sum_single0 below · cited by 11 · depth 14 - Multiplicity-freeness from two character sum identities
Finsupp.forall_apply_le_one_and_apply_one_eq_one_of_sum_eq_card_of_sum_mul_eq0 below · cited by 1 · depth 16 - Fibrewise zero-sum finitely supported ℤ-functions split into same-fibre differences
Finsupp.exists_list_eq_sum_single_sub_single_of_sum_fibre_eq_zero0 below · cited by 1 · depth 26 - Macaulay's bound for monomial sets one degree up
Finsupp.card_le_macaulayPow_card_of_forall_sub_single_mem0 below · cited by 1 · depth 33