chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections… · leanprover-community/mathlib4@88c4a94 · GitHub

Commit

chore(Data/Multiset/Basic): move the sub, union, inter sections…

Browse files

… lower (#19863)

* Move the sections about `sub`, `union` and `inter` under the sections about `count` and `filter`
* `Multiset.countP_sub` now has a different argument order to match `List.countP_diff`
* Golf `List.count_sub`
* Name the instances and declare them using `where` notation
* Define `Multiset.card` using `Quotient.lift`, not `Quotient.liftOn`

Loading branch information

YaelDillies committed Jan 6, 2025

1 parent baef601 commit 88c4a94