Commit 2023-03-19 17:35 03320fe2

View on Github →

chore: forward-port leanprover-community/mathlib#18429 (#2220) Also removes a duplicate lemma that was added by accident while porting.

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 def Multiset.Pi.empty
modified theorem Multiset.card_pi
modified theorem Multiset.mem_pi
deleted theorem Multiset.pi.con_ext
modified def Multiset.pi
modified theorem Multiset.pi_cons
modified theorem Multiset.pi_zero