Theorems · Definition · combinatorics
List.Vector.reverse
{α : Type u_1} → {n : ℕ} → List.Vector α n → List.Vector α nReverse a vector.
- Defined in
- Mathlib.Data.Vector.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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.toListproof · cited by 79
Cited by7
Results whose statement or proof uses this declaration.
- List.Vector.revInductionOn₂proof · cited by 15
- List.Vector.revInductionOnproof · cited by 6
- List.Vector.toList_reversestatement · cited by 0
- List.Vector.reverse_consstatement · cited by 0
- List.Vector.reverse_get_zerostatement and proof · cited by 0
- List.Vector.reverse_reversestatement and proof · cited by 0
- List.Vector.reverse_snocstatement · cited by 0