Theorem Multiset.card_strictMono

Modification history

2025-10-27 16:35
Mathlib/Data/Multiset/Defs.lean
feat(gcongr): support `@[gcongr]` for `Monotone` and friends (#28339) …
Modified Multiset.card_strictMonoView on Github →
2025-02-25 17:02
Mathlib/Data/Multiset/Basic.lean
chore(Data/Multiset): split `Multiset/Basic.lean` into many files (#22126) …
Modified Multiset.card_strictMonoView on Github →
2023-12-27 09:01
Mathlib/Data/Multiset/Basic.lean
chore: Improve `Finset` lemma names (#8894) …
Modified Multiset.card_strictMonoView on Github →
2023-12-09 13:26
Mathlib/Data/Multiset/Basic.lean
feat: Finsets and multisets are graded (#8892) …
Added Multiset.card_strictMonoView on Github →