Zulip Chat Archive

Stream: Is there code for X?

Topic: Matrix multiplication


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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: May 17 2021 at 15:13 UTC