Zulip Chat Archive

Stream: Is there code for X?

Topic: Matrix multiplication


Adam Topaz (Jan 15 2021 at 04:39):

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 (Jan 15 2021 at 05:00):

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 (Jan 15 2021 at 09:49):

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 (Jan 15 2021 at 14:28):

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


Last updated: Dec 20 2023 at 11:08 UTC