Annotating absence of instance

Stream: new members

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

no. what are you trying to do? #xy

[Yakov Pechersky]

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]

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]

there is no such thing.

[Kenny Lau]

this isn't a mathematical statement.

[Johan Commelin]

@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]

@Johan Commelin pointwise multiplication

[Johan Commelin]

Of course... silly me