mathlib
4c586d29 - chore(data/{multiset,finset}/pi): generalize from `Type` to `Sort` (#18429)

Commit
2 years ago
chore(data/{multiset,finset}/pi): generalize from `Type` to `Sort` (#18429) Everything in this file about `multiset.pi.cons` generalizes to `Sort`. The parts of the file which don't generalize now use `β` instead. This is motivated by #18417, though I do not know if supporting `Sort` is actually important there. Forward-ported as https://github.com/leanprover-community/mathlib4/pull/2220
Author
Parents
Loading