Matrix times vector simplification

Stream: new members

[Luiz Kazuo Takei]

I have a matrix and want to expand the first entry of the matrix multiplication by a generic vector.

def A : Matrix (Fin 2) (Fin 2) ℚ :=
    !![ 1, 2;
        3, 4]

example (x : Fin 2 → ℚ) : (A *ᵥ x) 0 = x 0 + 2 * x 1 := by
  sorry

AI helped me find one possible solution (shown below) using simp together with vecHead and vecTail:

example (x : Fin 2 → ℚ) : (A *ᵥ x) 0 = x 0 + 2 * x 1 := by
  simp[A, Matrix.mulVec, vecHead, vecTail]

While this works, I find that the use of vecHeadand vecTail(which are new to me) is counter-intuitive and diminishes readability. Is there an alternative way?

[Albert Smith]

if you're willing to change the goal slightly you can do the following:

example (x : Fin 2 → ℚ) : (A *ᵥ x) 0 = 1 * x 0 + 2 * x 1 := by
  rewrite [← mulVecᵣ_eq]; rfl

docs#Matrix.mulVecᵣ exists for essentially this purpose: A.mulVecᵣ x i is definitionally equal to A i 0 * x 0 + A i 1 * x 1 + ..., so that equality can be proven by rfl

[Luiz Kazuo Takei]

Thanks a lot! That worked very well and I learned something new! :slight_smile: