Zulip Chat Archive

Stream: new members

Topic: Matrix multiplication and zero vector


George Tsoukalas (Mar 14 2024 at 19:58):

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 (Mar 14 2024 at 20:42):

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

Jireh Loreaux (Mar 14 2024 at 20:44):

import Mathlib

open scoped Matrix

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

Jireh Loreaux (Mar 14 2024 at 20:46):

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 (Mar 14 2024 at 20:47):

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

Jireh Loreaux (Mar 14 2024 at 20:48):

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 *ᵥ).


Last updated: May 02 2025 at 03:31 UTC