Commit 2023-06-17 13:25 f3f3f1cb

View on Github →

feat: port Archive.Wiedijk100Theorems.Partition (#5173)

Estimated changes

Modified Archive.lean

Created Archive/Wiedijk100Theorems/Partition.lean

added theorem Theorems100.coeff_indicator

added theorem Theorems100.coeff_indicator_neg

added theorem Theorems100.coeff_indicator_pos

added theorem Theorems100.coeff_prod_range

added theorem Theorems100.constantCoeff_indicator

added def Theorems100.cut

added theorem Theorems100.cut_empty_succ

added theorem Theorems100.cut_equiv_antidiag

added theorem Theorems100.cut_insert

added theorem Theorems100.cut_univ_fin_eq_antidiagonalTuple

added theorem Theorems100.cut_zero

added theorem Theorems100.distinctGF_prop

added def Theorems100.indicatorSeries

added theorem Theorems100.mem_cut

added def Theorems100.mkOdd

added theorem Theorems100.num_series'

added theorem Theorems100.oddGF_prop

added def Theorems100.partialDistinctGF

added theorem Theorems100.partialDistinctGF_prop

added theorem Theorems100.partialGF_prop

added def Theorems100.partialOddGF

added theorem Theorems100.partialOddGF_prop

added theorem Theorems100.partition_theorem

added theorem Theorems100.same_coeffs

added theorem Theorems100.same_gf

added theorem Theorems100.two_series