Zulip Chat Archive

Stream: new members

Topic: Annotating absence of instance


Yakov Pechersky (Jun 16 2020 at 04:03):

If I wanted to formalize the statement that n x n matrices over have multiplication defined, but m x n do not, what would be the way to state that? That is, n x n matrices have a has_mul instance, but m x n, m \neq n do not (at least, by default in mathlib).

Kenny Lau (Jun 16 2020 at 04:04):

surely you can define a has_mul instance by just sending everything to 0

Yakov Pechersky (Jun 16 2020 at 04:05):

Of course. But at a particular point in a proof, if there are no matching instances in the instance cache, is there a way to state that in a non-error way?

Kenny Lau (Jun 16 2020 at 04:06):

no. what are you trying to do? #xy

Yakov Pechersky (Jun 16 2020 at 04:11):

Pretty much what I said. m x n matrices have addition and scalar multiplication defined. But only n x n matrices have multiplication also defined. I'm working on formalizing the statements in Gross's lectures. The statement at hand here is at https://youtu.be/EPQgeAz264g?list=PLA58AC5CABC1321A3&t=414 .

Yakov Pechersky (Jun 16 2020 at 04:13):

So what is the statement like m \neq n -> \not has_mul matrix (fin m) (fin n) \R, given a particular instance cache?

Kenny Lau (Jun 16 2020 at 04:13):

there is no such thing.

Kenny Lau (Jun 16 2020 at 04:13):

this isn't a mathematical statement.

Johan Commelin (Jun 16 2020 at 06:48):

@Yakov Pechersky You could try to formalise "there is no term of ring (matrix (fin m) (fin n) whose addition and zero are equal to the existing has_add and has_zero, unless m = n"
But I'll say upfront that I don't know if that statement is true.

Kenny Lau (Jun 16 2020 at 06:51):

@Johan Commelin pointwise multiplication

Johan Commelin (Jun 16 2020 at 06:57):

Of course... silly me


Last updated: Dec 20 2023 at 11:08 UTC