Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-07 13:46 10cf239e

View on Github →

feat(data/multiset): add Cartesian product over dependent functions

Estimated changes

modified theorem multiset.bind_bind
modified theorem multiset.bind_hcongr
added theorem multiset.card_pi
modified theorem multiset.map_hcongr
added theorem multiset.mem_pi
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
added theorem multiset.pi_cons
added theorem multiset.pi_zero