Commit 2023-01-13 17:44 5f6ad927

View on Github →

feat: port Data.Multiset.Pi (#1551)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Pi.lean

added def Multiset.Pi.cons

added theorem Multiset.Pi.cons_ne

added theorem Multiset.Pi.cons_same

added theorem Multiset.Pi.cons_swap

added def Multiset.Pi.empty

added theorem Multiset.card_pi

added theorem Multiset.mem_pi

added theorem Multiset.pi.con_ext

added theorem Multiset.pi.cons_ext

added def Multiset.pi

added theorem Multiset.pi_cons

added theorem Multiset.pi_cons_injective

added theorem Multiset.pi_zero