Matrix multiplication

Stream: Is there code for X?

[Adam Topaz]

Do we have any tools (tactics, lemmas, etc.) that make the following calculation not terrible?

import data.matrix.notation

variables {K : Type*} [field K] (x y : K)

def M := ![![(1 : K),0],![0,1]]
def V := matrix.col ![x,y]

example : matrix.mul M (V x y) = matrix.col ![x,y] := sorry

[Alex J. Best]

I think @Yakov Pechersky and @Eric Wieser were working on this sort of thing at #5593 which is almost all merged? Ah thats about det, not mul, still maybe some of it still applies.

[Anne Baanen]

There are a few simp rules in data.matrix.notation that try to do these computations, and in fact, it works here:

example : matrix.mul M (V x y) = matrix.col ![x,y] := by simp [M, V]

[Adam Topaz]

Great! Thanks @Anne Baanen . It didn't occur to me to simplify M and V as well :)