Commit 2023-01-20 12:30 7810d9d9

View on Github →

feat: port Data.Sym.Basic (#1672)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Sym/Basic.lean

added def Sym.Sym'

added def Sym.append

added theorem Sym.append_comm

added theorem Sym.append_inj_left

added theorem Sym.append_inj_right

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.cast_cast

added theorem Sym.cast_rfl

added theorem Sym.coe_append

added theorem Sym.coe_attach

added theorem Sym.coe_cast

added theorem Sym.coe_cons

added theorem Sym.coe_erase

added theorem Sym.coe_fill

added theorem Sym.coe_inj

added theorem Sym.coe_injective

added theorem Sym.coe_map

added theorem Sym.coe_nil

added theorem Sym.coe_replicate

added def Sym.cons'

added def Sym.cons

added theorem Sym.cons_equiv_eq_equiv_cons

added theorem Sym.cons_erase

added theorem Sym.cons_inj_left

added theorem Sym.cons_inj_right

added theorem Sym.cons_of_coe_eq

added theorem Sym.cons_swap

added theorem Sym.eq_nil_of_card_zero

added theorem Sym.eq_replicate

added theorem Sym.eq_replicate_iff

added theorem Sym.eq_replicate_of_subsingleton

added def Sym.equivCongr

added def Sym.erase

added theorem Sym.erase_cons_head

added theorem Sym.erase_mk

added theorem Sym.exists_eq_cons_of_succ

added theorem Sym.exists_mem

added theorem Sym.ext

added def Sym.fill

added theorem Sym.fill_filterNe

added def Sym.filterNe

added theorem Sym.filter_ne_fill

added def Sym.map

added theorem Sym.map_congr

added theorem Sym.map_cons

added theorem Sym.map_id'

added theorem Sym.map_id

added theorem Sym.map_injective

added theorem Sym.map_map

added theorem Sym.map_mk

added theorem Sym.map_zero

added theorem Sym.mem_append_iff

added theorem Sym.mem_attach

added theorem Sym.mem_cast

added theorem Sym.mem_coe

added theorem Sym.mem_cons

added theorem Sym.mem_cons_of_mem

added theorem Sym.mem_cons_self

added theorem Sym.mem_fill_iff

added theorem Sym.mem_map

added theorem Sym.mem_mk

added theorem Sym.mem_replicate

added def Sym.nil

added def Sym.ofVector

added theorem Sym.of_vector_cons

added theorem Sym.of_vector_nil

added def Sym.replicate

added theorem Sym.replicate_right_inj

added theorem Sym.replicate_right_injective

added theorem Sym.replicate_succ

added theorem Sym.sigma_sub_ext

added theorem Sym.sound

added def Sym.symEquivSym'

added theorem Sym.val_eq_coe

added def Sym

added def SymOptionSuccEquiv.decode

added theorem SymOptionSuccEquiv.decode_encode

added theorem SymOptionSuccEquiv.decode_inl

added theorem SymOptionSuccEquiv.decode_inr

added def SymOptionSuccEquiv.encode

added theorem SymOptionSuccEquiv.encode_decode

added theorem SymOptionSuccEquiv.encode_of_none_mem

added theorem SymOptionSuccEquiv.encode_of_not_none_mem

added def Vector.Perm.isSetoid

added def symOptionSuccEquiv

added def toMultiset