Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-28 10:33 b25bad7d

View on Github →

feat(archive/100-theorems-list): Partition theorem (#4259) A proof of Euler's partition theorem, from the Freek list. The proof is sorry-free but currently unpleasant, and some parts don't belong in archive/, so WIP for now.

Estimated changes

added theorem coeff_indicator
added theorem coeff_indicator_neg
added theorem coeff_indicator_pos
added theorem coeff_prod_range
added def cut
added theorem cut_empty_succ
added theorem cut_equiv_antidiag
added theorem cut_insert
added theorem cut_zero
added theorem distinct_gf_prop
added def indicator_series
added theorem mem_cut
added def mk_odd
added theorem num_series'
added theorem odd_gf_prop
added theorem partial_gf_prop
added def partial_odd_gf
added theorem partial_odd_gf_prop
added theorem partition_theorem
added theorem same_coeffs
added theorem same_gf
added theorem two_series
added theorem finset.mem_sum