Matrix multiplication and zero vector

Stream: new members

[George Tsoukalas]

Hi,

I am trying to get familiar with linear algebra in Lean and have run into some confusing problems. The first is the following:

example (n : ℕ) (M : Matrix (Fin n) (Fin n) ℂ) (v : Vector ℂ n) : M * v = v := sorry

which gives an error about matrix-vector multiplication:

failed to synthesize instance
  HMul (Matrix (Fin n) (Fin n) ℂ) (Vector ℂ n) ?m.2951861

I am not sure how to handle this - is Matrix - Vector multiplication defined a different way? The second problem I had was for this problem:

example (n : ℕ) (M : Matrix (Fin n) (Fin n) ℂ) (v : Vector ℂ n) : v + 0 = v := sorry

with error

failed to synthesize instance
  HAdd (Vector ℂ n) ℕ (Vector ℂ n)

Lean thinks that 0 is a natural number, but of course I want it to be the vector of 0s from \C. But Lean cannot infer it if I provide the right type either:

example (n : ℕ) (M : Matrix (Fin n) (Fin n) ℂ) (v : Vector ℂ n) : v + (0 : Vector ℂ n) = v := sorry

with error

failed to synthesize instance
  OfNat (Vector ℂ n) 0

failed to synthesize instance
  HAdd (Vector ℂ n) (Vector ℂ n) ?m.2784030

the second part leads me to think "Vector" is not the right class for what I want, it seems addition is not defined on it either? It would be great if there was a clean way to write the 0-vector given arbitrary n. Anyone know how to resolve these issues?

[Jireh Loreaux]

Probably you want M *ᵥ (0 : n → ℂ), where the notation *ᵥ is for docs#Matrix.mulVec

[Jireh Loreaux]

import Mathlib

open scoped Matrix

example (n : ℕ) (M : Matrix (Fin n) (Fin n) ℂ) : M *ᵥ 0 = 0 := Matrix.mulVec_zero M

[Jireh Loreaux]

docs#Vector is really about docs#List with a fixed length, but in general we don't use lists for things involving matrices.

[Jireh Loreaux]

Instead, the matrix version of a vector is v : n → ℂ.

[Jireh Loreaux]

You can multiply on the left with docs#Matrix.vecMul (with notation ᵥ* inside the Matrix scope) and on the right with docs#Matrix.mulVec (with notation *ᵥ).