Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-28 18:04 4c586d29

View on Github →

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

Estimated changes

modified theorem finset.mem_pi
modified def finset.pi
modified theorem finset.pi_empty
modified theorem finset.pi_insert
modified theorem finset.pi_subset
modified theorem finset.pi_val
modified theorem multiset.card_pi
modified theorem multiset.mem_pi
modified def multiset.pi.empty
modified def multiset.pi
modified theorem multiset.pi_cons
modified theorem multiset.pi_zero