Theorems · Theorem · combinatorics
List.Vector.get_eq_get_toList
∀ {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : Fin n), v.get i = v.toList.get (Fin.cast ⋯ i)- Defined in
- Mathlib.Data.Vector.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- List.Vectorstatement and proof · cited by 270
- List.Vector.toListstatement · cited by 79
- List.Vector.getstatement · cited by 41
- List.Vector.toList_lengthstatement · cited by 17
Cited by1
Results whose statement or proof uses this declaration.
- List.Vector.reverse_get_zeroproof · cited by 0