Commit 2026-02-10 11:37 1dc86631

View on Github →

feat(Data): factor Multiset.inf lemmas through to_dual (#34718) Derive Multiset.inf and its lemmas via to_dual from Multiset.sup, keeping names and attributes unchanged.

Estimated changes

deleted def Multiset.inf
deleted theorem Multiset.inf_add
deleted theorem Multiset.inf_coe
deleted theorem Multiset.inf_cons
deleted theorem Multiset.inf_dedup
deleted theorem Multiset.inf_le
deleted theorem Multiset.inf_mono
deleted theorem Multiset.inf_ndinsert
deleted theorem Multiset.inf_ndunion
deleted theorem Multiset.inf_singleton
deleted theorem Multiset.inf_union
deleted theorem Multiset.inf_zero
deleted theorem Multiset.le_inf