Commit 2023-11-24 20:37 9eed8c46

View on Github →

refactor: New Colex API (#7715) This fully rewrites Combinatorics.Colex to use a type synonym approach instead of abusing defeq. We also provide some API about initial segments of colex.

Estimated changes

added theorem Nat.geomSum_eq
added theorem Nat.geomSum_lt
deleted theorem Colex.colex_le_of_subset
deleted theorem Colex.colex_lt_of_ssubset
deleted theorem Colex.empty_toColex_le
deleted theorem Colex.empty_toColex_lt
deleted theorem Colex.eq_iff
deleted theorem Colex.hom_fin_le_iff
deleted theorem Colex.hom_fin_lt_iff
deleted theorem Colex.hom_le_iff
deleted theorem Colex.hom_lt_iff
deleted theorem Colex.le_def
deleted theorem Colex.le_trans
deleted theorem Colex.lt_def
deleted theorem Colex.lt_trans
deleted theorem Colex.lt_trichotomy
deleted theorem Colex.singleton_le_iff_le
deleted theorem Colex.singleton_lt_iff_lt
deleted def Colex.toColexRelHom
added theorem Finset.Colex.le_def
added structure Finset.Colex
deleted def Finset.Colex
added theorem Finset.ofColex_inj
added theorem Finset.ofColex_toColex
deleted def Finset.toColex
added theorem Finset.toColex_inj
added theorem Finset.toColex_ofColex
deleted theorem Nat.sum_two_pow_lt