Mathlib v3 is deprecated. Go to Mathlib v4

Theorem multiset.coe_append_eq_add_coe

Modification history

2018-09-21 17:46
data/multiset.lean
refactor(category/traversable): proofs about list instance for traverse, simplify multiset.traverse
Deleted multiset.coe_append_eq_add_coeView on Github →
2018-08-29 02:53
data/multiset.lean
feat(data/multiset): multisets are traversable using commutative, applicative functors (#220)
Added multiset.coe_append_eq_add_coeView on Github →