Theorems · Theorem · combinatorics
List.Vector.ext
∀ {α : Type u_1} {n : ℕ} {v w : List.Vector α n}, (∀ (m : Fin n), v.get m = w.get m) → v = wTwo v w : Vector α n are equal iff they are equal at every single index.
- Defined in
- Mathlib.Data.Vector.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Quot.sound
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.getstatement and proof · cited by 41
Cited by4
Results whose statement or proof uses this declaration.
- List.Vector.ofFn_getproof · cited by 8
- List.Vector.scanl_nilproof · cited by 2
- List.Vector.ext_iffproof · cited by 0
- List.Vector.zipWith_tailproof · cited by 0