Commit 2026-02-12 23:53 b4292a2e

View on Github →

feat(Finpartition): remove unnecessary DistribLattice assumptions (#34545) This PR weakens the typeclass assumptions of some lemmas and constructions:

  • generalizes exists_le_of_le and card_mono from DistribLattice to Lattice
  • generalizes extend from DistribLattice to IsModularLattice
  • generalizes combine from DistribLattice to IsModularLattice (this requires changing the argument from PairwiseDisjoint to SupIndep)
  • redefines bind using combine in a way that is defeq to the current definition

Estimated changes

modified def Finpartition.bind