Commit 2023-02-07 07:39 fbd57420

View on Github →

feat: port Data/Nat/Choose/Sum (#2121)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Choose/Sum.lean

added theorem Commute.add_pow'

added theorem Commute.add_pow

added theorem Finset.sum_powerset_apply_card

added theorem Finset.sum_powerset_neg_one_pow_card

added theorem Finset.sum_powerset_neg_one_pow_card_of_nonempty

added theorem Int.alternating_sum_range_choose

added theorem Int.alternating_sum_range_choose_of_ne

added theorem Nat.choose_middle_le_pow

added theorem Nat.four_pow_le_two_mul_add_one_mul_central_binom

added theorem Nat.sum_range_choose

added theorem Nat.sum_range_choose_halfway

added theorem add_pow