Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-07 13:46 be4a35fd

View on Github →

feat(data/multiset): add dependent recursor for multisets

Estimated changes

Modified data/list/basic.lean

Modified data/list/perm.lean

added theorem list.rec_heq_of_perm

Modified data/multiset.lean

added theorem multiset.rec_on_0

added theorem multiset.rec_on_cons