Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-21 17:46 568a15f8

View on Github →

refactor(category/traversable): proofs about list instance for traverse, simplify multiset.traverse

Estimated changes

Modified category/traversable/instances.lean

added theorem list.mem_traverse

added theorem list.traverse_append

added theorem list.traverse_cons

added theorem list.traverse_nil

deleted theorem traverse_append

Modified data/list/basic.lean

added theorem list.forall₂.flip

added theorem list.forall₂.mp

added theorem list.forall₂_and_left

deleted theorem list.forall₂_flip

Modified data/list/perm.lean

Modified data/multiset.lean

deleted theorem multiset.coe_append_eq_add_coe

deleted theorem multiset.coe_list_cons_eq_cons_coe

deleted theorem multiset.coe_traverse_cons

deleted theorem multiset.coe_traverse_cons_swap

modified def multiset.traverse