no goals
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
rw [cons_dotProduct_cons, cons_dotProduct_cons, dotProduct_empty, add_zero]