Multiplication of matrix by vector

Stream: new members

[Luiz Kazuo Takei]

I have the following code that works:

open Matrix
variable (k : ℚ)

#check !![k,k; k, k] *ᵥ ![k,k]

but if I try this it doesn't work:

open Matrix
variable (k : ℚ)

def B : Matrix (Fin 2) (Fin 2) ℚ := !![k,k;k,k]
def b : (Fin 2) → ℚ := ![k, k]

#check B *ᵥ b

I get the following error message:

Application type mismatch: The argument
  b
has type
  ℚ → Fin 2 → ℚ
but is expected to have type
  Fin 2 → Fin 2 → ℚ
in the application
  B *ᵥ b

Why?

[Robin Arnez]

variable adds the parameter k to both B and b so you end up with

import Mathlib

open Matrix

def B (k : ℚ) : Matrix (Fin 2) (Fin 2) ℚ := !![k,k;k,k]
def b (k : ℚ) : (Fin 2) → ℚ := ![k, k]

#check B *ᵥ b

where it should be a bit more obvious why it fails. Because of that, you need to specify k in the #check too:

import Mathlib

open Matrix
variable (k : ℚ)

def B : Matrix (Fin 2) (Fin 2) ℚ := !![k,k;k,k]
def b : (Fin 2) → ℚ := ![k, k]

#check B k *ᵥ b k -- works

[Luiz Kazuo Takei]

Thanks a lot!

So, if I understand correctly, when I do that, it views B and b as functions ℚ → Matrix (Fin 2) (Fin 2) ℚ and ℚ → (Fin 2) → ℚ respectively.

When we do math on paper, B would normally be viewed simply as Matrix (Fin 2) (Fin 2) ℚ. Is there a way to view such a B in this way?

[Eric Wieser]

You can use local notation "B" => !![k,k;k,k]:

import Mathlib

open Matrix
variable (k : ℚ)

local notation "B" => !![k,k;k,k]
local notation "b" => ![k, k]

#check B *ᵥ b

[Luiz Kazuo Takei]

Thanks a lot!