Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-27 12:07 b28734c8

View on Github →

feat(data/sym): Provide API for data.sym (#11032)

Estimated changes

Modified src/data/multiset/basic.lean

added theorem multiset.mem_repeat

added theorem multiset.repeat_left_inj

added theorem multiset.repeat_left_injective

Modified src/data/sym/basic.lean

added theorem sym.eq_nil_of_card_zero

added theorem sym.eq_repeat_of_subsingleton

added def sym.equiv_congr

added def sym.erase

added theorem sym.exists_eq_cons_of_succ

added def sym.map

added theorem sym.map_cons

added theorem sym.map_id

added theorem sym.map_map

added theorem sym.map_zero

added theorem sym.mem_map

added def sym.repeat

added theorem sym.repeat_left_inj

added theorem sym.repeat_left_injective

added theorem sym.repeat_succ

Modified src/data/sym/sym2.lean