Theorem Multiset.inf_dedup

Modification history

2026-02-10 11:37
Mathlib/Data/Multiset/Lattice.lean
feat(Data): factor `Multiset.inf` lemmas through `to_dual` (#34718) …
Deleted Multiset.inf_dedupView on Github →
2023-01-14 04:12
Mathlib/Data/Multiset/Lattice.lean
feat: port Data.Multiset.Lattice (#1556)
Added Multiset.inf_dedupView on Github →