# 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: May 14 2021 at 22:15 UTC