@[simp]

theorem Vector.sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = ↑n * a

theorem Vector.sum_append_int {n m : Nat} {as₁ : Vector Int n} {as₂ : Vector Int m} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum

theorem Vector.sum_reverse_int {n : Nat} (xs : Vector Int n) : xs.reverse.sum = xs.sum

theorem Vector.sum_eq_foldl_int {n : Nat} {xs : Vector Int n} : xs.sum = foldl (fun (x1 x2 : Int) => x1 + x2) 0 xs

@[simp]

theorem Vector.prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n

theorem Vector.prod_append_int {n m : Nat} {as₁ : Vector Int n} {as₂ : Vector Int m} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod

theorem Vector.prod_reverse_int {n : Nat} (xs : Vector Int n) : xs.reverse.prod = xs.prod

theorem Vector.prod_eq_foldl_int {n : Nat} {xs : Vector Int n} : xs.prod = foldl (fun (x1 x2 : Int) => x1 * x2) 1 xs