Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-10 15:29 62833ca5

View on Github →

feat(data/multiset): add relator

Estimated changes

Modified data/multiset.lean

added theorem multiset.card_eq_card_of_rel

added theorem multiset.cons_eq_cons

added theorem multiset.cons_ne_zero

added theorem multiset.rel.add

added theorem multiset.rel.mono

added inductive multiset.rel

added theorem multiset.rel_add_left

added theorem multiset.rel_add_right

added theorem multiset.rel_cons_left

added theorem multiset.rel_cons_right

added theorem multiset.rel_eq

added theorem multiset.rel_eq_refl

added theorem multiset.rel_flip

added theorem multiset.rel_flip_eq

added theorem multiset.rel_join

added theorem multiset.rel_map

added theorem multiset.rel_map_left

added theorem multiset.rel_map_right

added theorem multiset.rel_zero_left

added theorem multiset.rel_zero_right

added theorem multiset.zero_ne_cons

Modified tests/mk_iff_of_inductive.lean

deleted inductive multiset.rel