mathlib
01dfdb57 - chore(data/multiset/pi): generalize from `Type` to `Sort`

Commit

2 years ago

chore(data/multiset/pi): generalize from `Type` to `Sort`

Author

eric-wieser

eric-wieser

Committer

eric-wieser

eric-wieser

Parents

Loading