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