mathlib3
7c523cb7
- feat(data/list/count): partially sync with multiset (#18125)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
feat(data/list/count): partially sync with multiset (#18125) * rename `list.count_repeat` to `list.count_repeat_self`; * prove `list.count_repeat` with `if .. then .. else` in the RHS.
Author
urkud
Parents
5758ed34
Loading