Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-10 23:04 be22d07e

View on Github →

feat(data/sym/basic): some basic lemmas in preparation for stars and bars (#12479) Some lemmas extracted from @huynhtrankhanh's #11162, moved here to a separate PR

Estimated changes

added def sym.attach
added theorem sym.attach_cons
added theorem sym.attach_map_coe
added theorem sym.attach_mk
added theorem sym.attach_nil
added theorem sym.coe_attach
added theorem sym.coe_cons
added theorem sym.coe_erase
added theorem sym.coe_inj
added theorem sym.coe_injective
added theorem sym.coe_map
modified def sym.cons'
modified def sym.cons
modified theorem sym.cons_erase
modified def sym.equiv_congr
added theorem sym.erase_cons_head
added theorem sym.erase_mk
modified def sym.map
added theorem sym.map_congr
modified theorem sym.map_cons
added theorem sym.map_id'
modified theorem sym.map_id
added theorem sym.map_injective
added theorem sym.map_mk
modified theorem sym.map_zero
added theorem sym.mem_attach
modified theorem sym.mem_map
added theorem sym.mem_mk
added def sym.mk
modified def sym.sym'
modified def sym.sym_equiv_sym'
modified def sym
modified def vector.perm.is_setoid