instance Vector.instLawfulOrderOrd {α : Type u_1} [LE α] [LT α] [Ord α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Std.LawfulOrderOrd α] {n : Nat} : Std.LawfulOrderOrd (Vector α n)

@[instance_reducible]

instance Vector.instLinearOrderPackage {α : Type u_1} [LE α] [LT α] [Ord α] [h : BEq α] [DecidableEq α] [DecidableLT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Std.LawfulOrderOrd α] [Std.LawfulOrderBEq α] {n : Nat} : Std.LinearOrderPackage (Vector α n)