Basic

📁 Source: Mathlib/Data/Sym/Basic.lean

Statistics

Metric	Count
Definitions `isSetoid`, `Sym'`, `append`, `attach`, `cast`, `cons`, `cons'`, `decidableMem`, `equivCongr`, `erase`, `fill`, `filterNe`, `hasCoe`, `inhabitedSym`, `inhabitedSym'`, `instCoeVector`, `instEmptyCollectionOfNatNat`, `instMembership`, `instUnique`, `instZeroSym`, `map`, `mk`, `nil`, `ofVector`, `oneEquiv`, `replicate`, `symEquivSym'`, `toMultiset`, `uniqueZero`, `«term_::_»`, `«term_::ₛ_»`, `decode`, `encode`, `instDecidableEqSym`, `instDecidableRelVectorEquivOfDecidableEq`, `symOptionSuccEquiv`	36
Theorems `append_comm`, `append_inj_left`, `append_inj_right`, `attach_cons`, `attach_map_coe`, `attach_mk`, `attach_nil`, `card_coe`, `cast_cast`, `cast_rfl`, `coe_append`, `coe_attach`, `coe_cast`, `coe_cons`, `coe_erase`, `coe_fill`, `coe_inj`, `coe_injective`, `coe_map`, `coe_mk`, `coe_nil`, `coe_replicate`, `cons_equiv_eq_equiv_cons`, `cons_erase`, `cons_inj_left`, `cons_inj_right`, `cons_of_coe_eq`, `cons_swap`, `count_coe_fill_of_ne`, `count_coe_fill_self_of_notMem`, `eq_nil_of_card_zero`, `eq_replicate`, `eq_replicate_iff`, `eq_replicate_of_subsingleton`, `equivCongr_apply`, `equivCongr_symm_apply`, `erase_cons_head`, `erase_mk`, `exists`, `exists_cons_of_mem`, `exists_eq_cons_of_succ`, `exists_mem`, `ext`, `ext_iff`, `fill_filterNe`, `filter_ne_fill`, `forall`, `instIsEmptySucc`, `instNontrivialHAddNatOfNat`, `instSubsingleton`, `map_congr`, `map_cons`, `map_id`, `map_id'`, `map_injective`, `map_map`, `map_mk`, `map_zero`, `mem_append_iff`, `mem_attach`, `mem_cast`, `mem_coe`, `mem_cons`, `mem_cons_of_mem`, `mem_cons_self`, `mem_fill_iff`, `mem_map`, `mem_mk`, `mem_replicate`, `notMem_nil`, `ofVector_cons`, `ofVector_nil`, `oneEquiv_apply`, `replicate_right_inj`, `replicate_right_injective`, `replicate_succ`, `sigma_sub_ext`, `sound`, `toMultiset_zero`, `val_eq_coe`, `val_replicate`, `decode_encode`, `decode_inl`, `decode_inr`, `encode_decode`, `encode_of_none_mem`, `encode_of_none_notMem`	87
Total	123

List.Vector.Perm

Definitions

Name	Category	Theorems
`isSetoid` 📖	CompOp	—

Sym

Definitions

Name	Category	Theorems
`Sym'` 📖	CompOp	1 math math: `cons_equiv_eq_equiv_cons`
`append` 📖	CompOp	5 math math: `append_inj_right`, `append_inj_left`, `append_comm`, `mem_append_iff`, `coe_append`
`attach` 📖	CompOp	7 math math: `SymOptionSuccEquiv.encode_of_none_notMem`, `attach_mk`, `attach_nil`, `attach_map_coe`, `attach_cons`, `mem_attach`, `coe_attach`
`cast` 📖	CompOp	5 math math: `cast_rfl`, `cast_cast`, `mem_cast`, `append_comm`, `coe_cast`
`cons` 📖	CompOp	19 math math: `cons_swap`, `cons_inj_right`, `cons_erase`, `cons_inj_left`, `mem_cons_self`, `cons_equiv_eq_equiv_cons`, `SymOptionSuccEquiv.decode_inl`, `attach_cons`, `mem_cons_of_mem`, `List.sym_one_eq`, `replicate_succ`, `coe_cons`, `map_cons`, `Finset.sym_succ`, `mem_cons`, `exists_cons_of_mem`, `exists_eq_cons_of_succ`, `cons_of_coe_eq`, `ofVector_cons`
`cons'` 📖	CompOp	1 math math: `cons_equiv_eq_equiv_cons`
`decidableMem` 📖	CompOp	—
`equivCongr` 📖	CompOp	2 math math: `equivCongr_apply`, `equivCongr_symm_apply`
`erase` 📖	CompOp	5 math math: `cons_erase`, `erase_mk`, `SymOptionSuccEquiv.encode_of_none_mem`, `coe_erase`, `erase_cons_head`
`fill` 📖	CompOp	9 math math: `fill_filterNe`, `count_coe_fill_self_of_notMem`, `mem_fill_iff`, `coe_fill`, `count_coe_fill_of_ne`, `filter_ne_fill`, `Finset.sym_fill_mem`, `multinomial_coe_fill_of_notMem`, `Finset.symInsertEquiv_symm_apply_coe`
`filterNe` 📖	CompOp	5 math math: `fill_filterNe`, `filter_ne_fill`, `Finset.sym_filterNe_mem`, `Finset.symInsertEquiv_apply_snd_coe`, `Finset.symInsertEquiv_apply_fst`
`hasCoe` 📖	CompOp	—
`inhabitedSym` 📖	CompOp	—
`inhabitedSym'` 📖	CompOp	—
`instCoeVector` 📖	CompOp	—
`instEmptyCollectionOfNatNat` 📖	CompOp	1 math math: `Finset.sym_zero`
`instMembership` 📖	CompOp	16 math math: `mem_map`, `mem_fill_iff`, `mem_mk`, `mem_replicate`, `attach_nil`, `attach_map_coe`, `mem_cast`, `mem_cons_self`, `mem_append_iff`, `notMem_nil`, `exists_mem`, `attach_cons`, `mem_coe`, `mem_attach`, `mem_cons`, `coe_attach`
`instUnique` 📖	CompOp	—
`instZeroSym` 📖	CompOp	2 math math: `toMultiset_zero`, `map_zero`
`map` 📖	CompOp	18 math math: `SymOptionSuccEquiv.encode_of_none_notMem`, `map_id`, `mem_map`, `SymOptionSuccEquiv.decode_inr`, `equivCongr_apply`, `attach_map_coe`, `map_id'`, `map_injective`, `List.sym_map`, `map_zero`, `Nat.Partition.ofSym_map`, `coe_map`, `equivCongr_symm_apply`, `map_congr`, `attach_cons`, `map_map`, `map_cons`, `map_mk`
`mk` 📖	CompOp	—
`nil` 📖	CompOp	6 math math: `ofVector_nil`, `attach_nil`, `eq_nil_of_card_zero`, `notMem_nil`, `coe_nil`, `List.sym_one_eq`
`ofVector` 📖	CompOp	4 math math: `ofVector_nil`, `cons_of_coe_eq`, `sound`, `ofVector_cons`
`oneEquiv` 📖	CompOp	1 math math: `oneEquiv_apply`
`replicate` 📖	CompOp	12 math math: `eq_replicate_iff`, `Finset.replicate_mem_sym`, `coe_fill`, `mem_replicate`, `Finset.sym_singleton`, `eq_replicate_of_subsingleton`, `replicate_right_injective`, `replicate_succ`, `replicate_right_inj`, `coe_replicate`, `eq_replicate`, `val_replicate`
`symEquivSym'` 📖	CompOp	1 math math: `cons_equiv_eq_equiv_cons`
`toMultiset` 📖	CompOp	30 math math: `toMultiset_zero`, `val_eq_coe`, `coe_equivNatSumOfFintype_apply_apply`, `coe_equivNatSum_apply_apply`, `count_coe_fill_self_of_notMem`, `coe_equivNatSum_symm_apply`, `Finset.map_sym_eq_piAntidiag`, `DividedPowers.dpow_sum'`, `coe_equivNatSumOfFintype_symm_apply`, `Finset.sum_count_of_mem_sym`, `coe_mk`, `coe_fill`, `coe_inj`, `norm_iteratedFDerivWithin_prod_le`, `DividedPowers.dpow_sum`, `count_coe_fill_of_ne`, `coe_map`, `coe_erase`, `norm_iteratedFDeriv_prod_le`, `multinomial_coe_fill_of_notMem`, `coe_injective`, `coe_nil`, `coe_cons`, `coe_cast`, `mem_coe`, `coe_replicate`, `coe_append`, `ext_iff`, `coe_attach`, `card_coe`
`uniqueZero` 📖	CompOp	—
`«term_::_»` 📖	CompOp	—
`«term_::ₛ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_comm` 📖	mathematical	—	`append` `DFunLike.coe` `Equiv` `Sym` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Nat.instAddCommSemigroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `cast` `add_comm`	—	`add_comm` `cast_rfl`
`append_inj_left` 📖	mathematical	—	`append`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`append_inj_right` 📖	mathematical	—	`append`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd`
`attach_cons` 📖	mathematical	—	`attach` `cons` `Sym` `instMembership` `mem_cons_self` `map` `mem_cons_of_mem` `Subtype.prop`	—	`coe_injective` `mem_cons_self` `mem_cons_of_mem` `Subtype.prop` `Multiset.attach_cons`
`attach_map_coe` 📖	mathematical	—	`map` `Sym` `instMembership` `attach`	—	`coe_injective` `Multiset.attach_map_val`
`attach_mk` 📖	mathematical	`Multiset.card`	`attach` `Multiset` `Multiset.instMembership` `Multiset.attach` `Multiset.card_attach`	—	—
`attach_nil` 📖	mathematical	—	`attach` `nil` `Sym` `instMembership`	—	—
`card_coe` 📖	mathematical	—	`Multiset.card` `toMultiset`	—	`Subtype.prop`
`cast_cast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `cast`	—	—
`cast_rfl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `cast`	—	—
`coe_append` 📖	mathematical	—	`toMultiset` `append` `Multiset` `Multiset.instAdd`	—	—
`coe_attach` 📖	mathematical	—	`toMultiset` `Sym` `instMembership` `attach` `Multiset.attach`	—	—
`coe_cast` 📖	mathematical	—	`toMultiset` `DFunLike.coe` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `cast`	—	—
`coe_cons` 📖	mathematical	—	`toMultiset` `cons` `Multiset.cons`	—	—
`coe_erase` 📖	mathematical	`Sym` `instMembership`	`toMultiset` `erase` `Multiset.erase`	—	—
`coe_fill` 📖	mathematical	—	`toMultiset` `fill` `Multiset` `Multiset.instAdd` `replicate`	—	—
`coe_inj` 📖	mathematical	—	`toMultiset`	—	`coe_injective`
`coe_injective` 📖	mathematical	—	`Sym` `Multiset` `toMultiset`	—	`Subtype.coe_injective`
`coe_map` 📖	mathematical	—	`toMultiset` `map` `Multiset.map`	—	—
`coe_mk` 📖	mathematical	`Multiset.card`	`toMultiset`	—	—
`coe_nil` 📖	mathematical	—	`toMultiset` `nil` `Multiset` `Multiset.instZero`	—	—
`coe_replicate` 📖	mathematical	—	`toMultiset` `replicate` `Multiset.replicate`	—	—
`cons_equiv_eq_equiv_cons` 📖	mathematical	—	`cons'` `DFunLike.coe` `Equiv` `Sym` `Sym'` `EquivLike.toFunLike` `Equiv.instEquivLike` `symEquivSym'` `cons`	—	—
`cons_erase` 📖	mathematical	`Sym` `instMembership`	`cons` `erase`	—	`coe_injective` `Multiset.cons_erase`
`cons_inj_left` 📖	mathematical	—	`cons`	—	`Multiset.cons_inj_left`
`cons_inj_right` 📖	mathematical	—	`cons`	—	`Multiset.cons_inj_right`
`cons_of_coe_eq` 📖	mathematical	—	`cons` `ofVector` `List.Vector.cons`	—	—
`cons_swap` 📖	mathematical	—	`cons`	—	`Multiset.cons_swap`
`count_coe_fill_of_ne` 📖	mathematical	—	`Multiset.count` `toMultiset` `fill`	—	`Multiset.count_add` `Multiset.count_eq_zero_of_notMem` `add_zero`
`count_coe_fill_self_of_notMem` 📖	mathematical	`Sym` `instMembership`	`Multiset.count` `toMultiset` `fill`	—	`Multiset.count_add` `Multiset.count_eq_zero_of_notMem` `Multiset.count_replicate_self` `zero_add`
`eq_nil_of_card_zero` 📖	mathematical	—	`nil`	—	`Multiset.card_eq_zero`
`eq_replicate` 📖	mathematical	—	`replicate`	—	`Multiset.eq_replicate` `Subtype.prop`
`eq_replicate_iff` 📖	mathematical	—	`replicate`	—	`val_replicate` `Multiset.eq_replicate`
`eq_replicate_of_subsingleton` 📖	mathematical	—	`replicate`	—	`eq_replicate`
`equivCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivCongr` `map`	—	—
`equivCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivCongr` `map`	—	—
`erase_cons_head` 📖	mathematical	`Sym` `instMembership` `cons` `mem_cons_self`	`erase`	—	`coe_injective` `Multiset.erase_cons_head`
`erase_mk` 📖	mathematical	`Multiset.card` `Multiset` `Multiset.instMembership`	`erase` `Multiset.erase`	—	—
`exists` 📖	—	—	—	—	—
`exists_cons_of_mem` 📖	mathematical	`Sym` `instMembership`	`cons`	—	`Multiset.exists_cons_of_mem` `AddRightCancelSemigroup.toIsRightCancelAdd` `Multiset.card_cons`
`exists_eq_cons_of_succ` 📖	mathematical	—	`cons`	—	`exists_mem` `cons_erase`
`exists_mem` 📖	mathematical	—	`Sym` `instMembership`	—	`Multiset.card_pos_iff_exists_mem`
`ext` 📖	—	`toMultiset`	—	—	`coe_injective`
`ext_iff` 📖	mathematical	—	`toMultiset`	—	`ext`
`fill_filterNe` 📖	mathematical	—	`fill` `Sym` `filterNe`	—	`ext` `coe_fill` `filterNe.eq_1` `val_eq_coe` `Multiset.ext'` `Multiset.count_add` `Multiset.count_filter` `coe_replicate` `Multiset.count_replicate` `eq_or_ne` `zero_add` `add_zero`
`filter_ne_fill` 📖	mathematical	`Sym` `instMembership`	`filterNe` `fill`	—	`sigma_sub_ext` `filterNe.eq_1` `val_eq_coe` `coe_fill` `Multiset.filter_add` `Multiset.filter_eq_self` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Multiset.eq_zero_iff_forall_notMem` `mem_replicate` `mem_coe` `Multiset.mem_filter`
`forall` 📖	—	—	—	—	—
`instIsEmptySucc` 📖	mathematical	—	`IsEmpty` `Sym`	—	`exists_mem`
`instNontrivialHAddNatOfNat` 📖	mathematical	—	`Nontrivial` `Sym`	—	`Function.Injective.nontrivial` `replicate_right_injective`
`instSubsingleton` 📖	mathematical	—	`Sym`	—	`Unique.instSubsingleton` `exists_mem` `eq_replicate_of_subsingleton`
`map_congr` 📖	mathematical	—	`map`	—	`Multiset.map_congr`
`map_cons` 📖	mathematical	—	`map` `cons`	—	`ext` `Multiset.map_cons`
`map_id` 📖	mathematical	—	`map`	—	`ext` `Multiset.map_congr` `Multiset.map_id'`
`map_id'` 📖	mathematical	—	`map`	—	`ext` `Multiset.map_id'`
`map_injective` 📖	mathematical	—	`Sym` `map`	—	`coe_injective` `Multiset.map_injective`
`map_map` 📖	mathematical	—	`map`	—	`Multiset.map_map` `Multiset.map_congr`
`map_mk` 📖	mathematical	`Multiset.card`	`map` `Multiset.map`	—	—
`map_zero` 📖	mathematical	—	`map` `Sym` `instZeroSym`	—	—
`mem_append_iff` 📖	mathematical	—	`Sym` `instMembership` `append`	—	`Multiset.mem_add`
`mem_attach` 📖	mathematical	—	`Sym` `instMembership` `attach`	—	`Multiset.mem_attach`
`mem_cast` 📖	mathematical	—	`Sym` `instMembership` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `cast`	—	—
`mem_coe` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `toMultiset` `Sym` `instMembership`	—	—
`mem_cons` 📖	mathematical	—	`Sym` `instMembership` `cons`	—	`Multiset.mem_cons`
`mem_cons_of_mem` 📖	mathematical	`Sym` `instMembership`	`cons`	—	`Multiset.mem_cons_of_mem`
`mem_cons_self` 📖	mathematical	—	`Sym` `instMembership` `cons`	—	`Multiset.mem_cons_self`
`mem_fill_iff` 📖	mathematical	—	`Sym` `instMembership` `fill`	—	`fill.eq_1` `mem_cast` `mem_append_iff` `mem_replicate`
`mem_map` 📖	mathematical	—	`Sym` `instMembership` `map`	—	`Multiset.mem_map`
`mem_mk` 📖	mathematical	`Multiset.card`	`Sym` `instMembership` `Multiset` `Multiset.instMembership`	—	—
`mem_replicate` 📖	mathematical	—	`Sym` `instMembership` `replicate`	—	`Multiset.mem_replicate`
`notMem_nil` 📖	mathematical	—	`Sym` `instMembership` `nil`	—	`Multiset.notMem_zero`
`ofVector_cons` 📖	mathematical	—	`ofVector` `List.Vector.cons` `cons`	—	—
`ofVector_nil` 📖	mathematical	—	`ofVector` `List.Vector.nil` `nil`	—	—
`oneEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `oneEquiv` `Multiset` `Multiset.card` `Multiset.instSingleton`	—	—
`replicate_right_inj` 📖	mathematical	—	`replicate`	—	—
`replicate_right_injective` 📖	mathematical	—	`Sym` `replicate`	—	—
`replicate_succ` 📖	mathematical	—	`replicate` `cons`	—	—
`sigma_sub_ext` 📖	—	`toMultiset` `Sym`	—	—	`Sigma.subtype_ext` `val_eq_coe`
`sound` 📖	mathematical	—	`ofVector`	—	—
`toMultiset_zero` 📖	mathematical	—	`toMultiset` `Sym` `instZeroSym` `Multiset` `Multiset.instZero`	—	—
`val_eq_coe` 📖	mathematical	—	`Multiset` `Multiset.card` `toMultiset`	—	—
`val_replicate` 📖	mathematical	—	`Multiset` `Multiset.card` `replicate` `Multiset.replicate`	—	`val_eq_coe` `coe_replicate`

SymOptionSuccEquiv

Definitions

Name	Category	Theorems
`decode` 📖	CompOp	4 math math: `encode_decode`, `decode_inr`, `decode_encode`, `decode_inl`
`encode` 📖	CompOp	4 math math: `encode_of_none_notMem`, `encode_decode`, `decode_encode`, `encode_of_none_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decode_encode` 📖	mathematical	—	`decode` `encode`	—	`encode_of_none_mem` `Sym.cons_erase` `encode_of_none_notMem` `Sym.map_congr` `Sym.map_map` `Sym.attach_map_coe`
`decode_inl` 📖	mathematical	—	`decode` `Sym` `Sym.cons`	—	—
`decode_inr` 📖	mathematical	—	`decode` `Sym` `Sym.map` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Function.Embedding.some`	—	—
`encode_decode` 📖	mathematical	—	`encode` `decode`	—	`encode_of_none_mem` `Sym.erase_cons_head` `Multiset.mem_map` `Sym.map_injective` `Option.some_injective` `Sym.map_congr` `Sym.map_map` `Sym.attach_map_coe`
`encode_of_none_mem` 📖	mathematical	`Sym` `Sym.instMembership`	`encode` `Sym.erase`	—	—
`encode_of_none_notMem` 📖	mathematical	`Sym` `Sym.instMembership`	`encode` `Sym.map` `Sym.attach`	—	—

(root)

Definitions

Name	Category	Theorems
`instDecidableEqSym` 📖	CompOp	3 math math: `Finset.sym_union`, `Finset.sym_inter`, `Finset.sym_succ`
`instDecidableRelVectorEquivOfDecidableEq` 📖	CompOp	—
`symOptionSuccEquiv` 📖	CompOp	—

---

← Back to Index