Basic

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

Statistics

Metric	Count
Definitions `vectorEquivFin`, `casesOn`, `casesOn₂`, `casesOn₃`, `inductionOn`, `inductionOn₂`, `inductionOn₃`, `insertIdx`, `instInhabited`, `instTraversableFlipNat`, `last`, `mOfFn`, `mmap`, `reverse`, `scanl`, `toArray`, `traverse`, `«term_::ᵥ_»`	18
Theorems `append_nil`, `comp_traverse`, `cons_val`, `empty_toList_eq_ff`, `eq_cons_iff`, `eraseIdx_insertIdx'`, `eraseIdx_insertIdx_self`, `eraseIdx_val`, `exists_eq_cons`, `ext`, `ext_iff`, `getElem_map`, `getElem_pmap`, `get_append_cons_succ`, `get_append_cons_zero`, `get_cons_nil`, `get_cons_succ`, `get_cons_zero`, `get_eq_get_toList`, `get_map`, `get_map₂`, `get_ofFn`, `get_replicate`, `get_set_eq_if`, `get_set_of_ne`, `get_set_same`, `get_tail`, `get_tail_succ`, `get_zero`, `head?_toList`, `head_map`, `head_ofFn`, `head_pmap`, `id_traverse`, `inductionOn_cons`, `inductionOn_nil`, `insertIdx_comm`, `insertIdx_val`, `instLawfulTraversableFlipNat`, `last_def`, `length_val`, `mOfFn_pure`, `mapAccumr_cons`, `mapAccumr₂_cons`, `map_id`, `map₂_cons`, `map₂_nil`, `mk_toList`, `mmap_cons`, `mmap_nil`, `naturality`, `ne_cons_iff`, `nodup_iff_injective_get`, `not_empty_toList`, `ofFn_get`, `pmap_cons`, `pmap_cons'`, `prod_set`, `prod_set'`, `replicate_succ`, `reverse_get_zero`, `reverse_reverse`, `scanl_cons`, `scanl_get`, `scanl_head`, `scanl_nil`, `scanl_singleton`, `scanl_val`, `singleton_tail`, `sum_set`, `sum_set'`, `tail_map`, `tail_nil`, `tail_ofFn`, `tail_pmap`, `tail_val`, `toList_empty`, `toList_injective`, `toList_map`, `toList_ofFn`, `toList_pmap`, `toList_reverse`, `toList_scanl`, `toList_set`, `toList_singleton`, `toList_tail`, `traverse_def`, `traverse_eq_map_id`, `zero_subsingleton`	89
Total	107

Equiv

Definitions

Name	Category	Theorems
`vectorEquivFin` 📖	CompOp	—

List.Vector

Definitions

Name	Category	Theorems
`casesOn` 📖	CompOp	—
`casesOn₂` 📖	CompOp	—
`casesOn₃` 📖	CompOp	—
`inductionOn` 📖	CompOp	2 math math: `inductionOn_cons`, `inductionOn_nil`
`inductionOn₂` 📖	CompOp	—
`inductionOn₃` 📖	CompOp	—
`insertIdx` 📖	CompOp	7 math math: `continuous_insertIdx'`, `eraseIdx_insertIdx'`, `insertIdx_comm`, `tendsto_insertIdx`, `continuous_insertIdx`, `insertIdx_val`, `eraseIdx_insertIdx_self`
`instInhabited` 📖	CompOp	—
`instTraversableFlipNat` 📖	CompOp	1 math math: `instLawfulTraversableFlipNat`
`last` 📖	CompOp	2 math math: `last_def`, `reverse_get_zero`
`mOfFn` 📖	CompOp	3 math math: `mOfFn_pure`, `Turing.ToPartrec.Code.exists_code.comp`, `Vector.mOfFn_part_some`
`mmap` 📖	CompOp	2 math math: `mmap_cons`, `mmap_nil`
`reverse` 📖	CompOp	5 math math: `reverse_reverse`, `reverse_cons`, `reverse_get_zero`, `toList_reverse`, `reverse_snoc`
`scanl` 📖	CompOp	7 math math: `scanl_get`, `scanl_nil`, `scanl_head`, `scanl_singleton`, `scanl_val`, `toList_scanl`, `scanl_cons`
`toArray` 📖	CompOp	—
`traverse` 📖	CompOp	5 math math: `traverse_def`, `naturality`, `traverse_eq_map_id`, `id_traverse`, `comp_traverse`
`«term_::ᵥ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_nil` 📖	mathematical	—	`List.Vector` `instHAppendHAddNat` `nil`	—	—
`comp_traverse` 📖	mathematical	—	`traverse` `Functor.Comp` `Functor.Comp.instApplicativeComp` `List.Vector`	—	`traverse_def` `seq_map_assoc` `map_seq`
`cons_val` 📖	mathematical	—	`cons`	—	—
`empty_toList_eq_ff` 📖	mathematical	—	`toList`	—	—
`eq_cons_iff` 📖	mathematical	—	`cons` `head` `tail`	—	`head_cons` `tail_cons` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `cons_head_tail`
`eraseIdx_insertIdx'` 📖	mathematical	—	`eraseIdx` `Fin.succAbove` `insertIdx` `Fin.predAbove`	—	`lt_of_le_of_lt` `length_val`
`eraseIdx_insertIdx_self` 📖	mathematical	—	`eraseIdx` `insertIdx`	—	—
`eraseIdx_val` 📖	mathematical	—	`eraseIdx`	—	—
`exists_eq_cons` 📖	mathematical	—	`cons`	—	`eq_cons_iff`
`ext` 📖	—	`get`	—	—	—
`ext_iff` 📖	mathematical	—	`get`	—	`ext`
`getElem_map` 📖	mathematical	—	`List.Vector` `instGetElemNatLt` `map`	—	`toList_map`
`getElem_pmap` 📖	mathematical	—	`List.Vector` `instGetElemNatLt` `pmap`	—	`toList_pmap`
`get_append_cons_succ` 📖	mathematical	—	`get` `List.Vector` `instHAppendHAddNat` `cons`	—	—
`get_append_cons_zero` 📖	mathematical	—	`get` `List.Vector` `instHAppendHAddNat` `cons`	—	—
`get_cons_nil` 📖	mathematical	—	`get` `cons` `nil`	—	—
`get_cons_succ` 📖	mathematical	—	`get` `cons`	—	`get_tail_succ` `tail_cons`
`get_cons_zero` 📖	mathematical	—	`get` `cons`	—	`get_zero` `head_cons`
`get_eq_get_toList` 📖	mathematical	—	`get` `toList` `toList_length`	—	—
`get_map` 📖	mathematical	—	`get` `map`	—	`toList_length`
`get_map₂` 📖	mathematical	—	`get` `map₂`	—	`map₂_cons` `get_zero` `head_cons` `get_cons_succ`
`get_ofFn` 📖	mathematical	—	`get` `ofFn`	—	`toList_length` `toList_ofFn`
`get_replicate` 📖	mathematical	—	`get` `replicate`	—	—
`get_set_eq_if` 📖	mathematical	—	`get` `set`	—	`get_set_same` `get_set_of_ne`
`get_set_of_ne` 📖	mathematical	—	`get` `set`	—	`toList_length` `List.getElem_set_of_ne`
`get_set_same` 📖	mathematical	—	`get` `set`	—	`toList_length`
`get_tail` 📖	mathematical	—	`get` `tail`	—	—
`get_tail_succ` 📖	mathematical	—	`get` `tail`	—	`toList_length`
`get_zero` 📖	mathematical	—	`get` `head`	—	—
`head?_toList` 📖	mathematical	—	`toList` `head`	—	—
`head_map` 📖	mathematical	—	`head` `map`	—	`exists_eq_cons` `map_cons` `head_cons`
`head_ofFn` 📖	mathematical	—	`head` `ofFn`	—	`get_zero` `get_ofFn`
`head_pmap` 📖	mathematical	—	`head` `pmap`	—	`exists_eq_cons` `pmap.congr_simp` `head_cons`
`id_traverse` 📖	mathematical	—	`traverse` `List.Vector`	—	`CommApplicative.toLawfulApplicative` `instCommApplicativeId`
`inductionOn_cons` 📖	mathematical	—	`inductionOn` `cons`	—	—
`inductionOn_nil` 📖	mathematical	—	`inductionOn` `nil`	—	—
`insertIdx_comm` 📖	mathematical	—	`insertIdx`	—	—
`insertIdx_val` 📖	mathematical	—	`insertIdx`	—	—
`instLawfulTraversableFlipNat` 📖	mathematical	—	`LawfulTraversable` `List.Vector` `instTraversableFlipNat`	—	`id_traverse` `comp_traverse` `traverse_eq_map_id` `naturality`
`last_def` 📖	mathematical	—	`last` `get`	—	—
`length_val` 📖	—	—	—	—	—
`mOfFn_pure` 📖	mathematical	—	`mOfFn` `List.Vector` `ofFn`	—	`mOfFn.eq_2` `ofFn.eq_2`
`mapAccumr_cons` 📖	mathematical	—	`mapAccumr` `cons`	—	—
`mapAccumr₂_cons` 📖	mathematical	—	`mapAccumr₂` `cons`	—	—
`map_id` 📖	mathematical	—	`map`	—	`eq` `toList_map`
`map₂_cons` 📖	mathematical	—	`map₂` `cons`	—	—
`map₂_nil` 📖	mathematical	—	`map₂` `nil`	—	—
`mk_toList` 📖	—	`toList`	—	—	—
`mmap_cons` 📖	mathematical	—	`mmap` `cons` `List.Vector`	—	—
`mmap_nil` 📖	mathematical	—	`mmap` `nil` `List.Vector`	—	—
`naturality` 📖	mathematical	—	`List.Vector` `traverse`	—	`ApplicativeTransformation.preserves_pure` `traverse_def` `ApplicativeTransformation.preserves_seq` `ApplicativeTransformation.preserves_map`
`ne_cons_iff` 📖	—	—	—	—	`eq_cons_iff` `not_and_or`
`nodup_iff_injective_get` 📖	mathematical	—	`toList` `get`	—	`List.nodup_iff_injective_get`
`not_empty_toList` 📖	mathematical	—	`toList`	—	`empty_toList_eq_ff` `Bool.coe_sort_false`
`ofFn_get` 📖	mathematical	—	`ofFn` `get`	—	`ext` `get_ofFn`
`pmap_cons` 📖	mathematical	—	`pmap` `cons`	—	—
`pmap_cons'` 📖	mathematical	—	`cons` `pmap`	—	—
`prod_set` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `toList` `set` `take` `drop`	—	`List.prod_set` `toList_length` `toList_take` `toList_drop`
`prod_set'` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `toList` `set` `InvOneClass.toInv` `get`	—	`List.prod_set'` `toList_length` `mul_assoc`
`replicate_succ` 📖	mathematical	—	`replicate` `cons`	—	—
`reverse_get_zero` 📖	mathematical	—	`head` `reverse` `last`	—	`get_zero` `last_def` `toList_length` `get_eq_get_toList`
`reverse_reverse` 📖	mathematical	—	`reverse`	—	—
`scanl_cons` 📖	mathematical	—	`scanl` `cons`	—	`eq` `toList_cons`
`scanl_get` 📖	mathematical	—	`get` `scanl`	—	`Fin.eq_zero` `scanl_singleton` `get_zero` `head_cons` `toList_cons` `toList_singleton` `zero_add` `cons_head_tail` `scanl_cons` `get_cons_succ` `scanl_head`
`scanl_head` 📖	mathematical	—	`head` `scanl`	—	`zero_subsingleton` `head_cons` `cons_head_tail` `toList_length` `toList_cons` `scanl_cons`
`scanl_nil` 📖	mathematical	—	`scanl` `nil` `cons`	—	—
`scanl_singleton` 📖	mathematical	—	`scanl` `cons` `head` `nil`	—	`cons_head_tail` `singleton_tail` `scanl_cons` `head_cons`
`scanl_val` 📖	mathematical	—	`scanl`	—	—
`singleton_tail` 📖	mathematical	—	`tail` `nil`	—	—
`sum_set` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero` `toList` `set` `take` `drop`	—	`List.sum_set` `toList_length` `toList_take` `toList_drop`
`sum_set'` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `toList` `set` `NegZeroClass.toNeg` `get`	—	`List.sum_set'` `toList_length` `add_assoc`
`tail_map` 📖	mathematical	—	`tail` `map`	—	`exists_eq_cons` `map_cons` `tail_cons`
`tail_nil` 📖	mathematical	—	`tail` `nil`	—	—
`tail_ofFn` 📖	mathematical	—	`tail` `ofFn`	—	`ofFn_get` `get_tail` `get_ofFn`
`tail_pmap` 📖	mathematical	—	`tail` `pmap`	—	`exists_eq_cons` `pmap.congr_simp` `tail_cons`
`tail_val` 📖	mathematical	—	`tail`	—	—
`toList_empty` 📖	mathematical	—	`toList`	—	—
`toList_injective` 📖	mathematical	—	`List.Vector` `toList`	—	`Subtype.val_injective`
`toList_map` 📖	mathematical	—	`toList` `map`	—	—
`toList_ofFn` 📖	mathematical	—	`toList` `ofFn`	—	`ofFn.eq_1` `toList.eq_1` `nil.eq_1` `ofFn.eq_2` `toList_cons`
`toList_pmap` 📖	mathematical	—	`toList` `pmap`	—	—
`toList_reverse` 📖	mathematical	—	`toList` `reverse`	—	—
`toList_scanl` 📖	mathematical	—	`toList` `scanl`	—	—
`toList_set` 📖	mathematical	—	`toList` `set`	—	—
`toList_singleton` 📖	mathematical	—	`toList` `head`	—	`cons_head_tail` `singleton_tail` `toList_cons` `head_cons`
`toList_tail` 📖	mathematical	—	`toList` `tail`	—	—
`traverse_def` 📖	mathematical	—	`traverse` `cons` `List.Vector`	—	—
`traverse_eq_map_id` 📖	mathematical	—	`traverse` `List.Vector` `map`	—	`CommApplicative.toLawfulApplicative` `instCommApplicativeId`
`zero_subsingleton` 📖	mathematical	—	`List.Vector`	—	`ext`

---

← Back to Index