# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: nonzero (fin n.succ.succ)

#### Yakov Pechersky (Jun 28 2020 at 20:19):

Is there no `instance nonzero (fin n.succ.succ)`

defined anywhere? Proving `0 \ne 1`

for those sorts of `fin`

types would be much easier. Should something like this go `data/fin`

?

```
instance nonzero_fin {n : ℕ} : nonzero (fin n.succ.succ) :=
⟨λ h, by { rw fin.eq_iff_veq at h, exact zero_ne_one h }⟩
```

#### Alex J. Best (Jun 28 2020 at 20:41):

I think if you want to use `fin n`

as a ring using `zmod`

instead works better as it has more support, there is docs#zmod.nonzero for instance, which takes `fact (1 < n)`

as a (typeclass) argument.

#### Yakov Pechersky (Jun 28 2020 at 20:43):

It's really trying to get `matrix.one_val_ne`

to work in a pleasant way for matrices of `fin 2`

or larger.

#### Alex J. Best (Jun 28 2020 at 20:48):

In that case it sounds like you aren't really using the ring structure? You just want to say that if the cardinality of a fintype is at least 2 then [something]? I guess the mathlib way is not to prefer `fin n`

as the indexing set of a matrix over any other fintype.

#### Alex J. Best (Jun 28 2020 at 20:49):

Or maybe I misunderstood, do you want matrices valued in `fin n`

or with `fin n`

as the index set?

#### Yakov Pechersky (Jun 28 2020 at 21:54):

I understand that matrices can be indexed with any fintype. It's easiest to instantiate a matrix of a fixed dimension with fin n, unless I don't understand something

#### Alex J. Best (Jun 28 2020 at 21:57):

Sure if you want an explicit matrix to play with thats definitely true, but as you mentioned "get matrix.one_val_ne to work" I thought you wanted to prove a library result about something. If you say a bit more what you mean by getting that result to work it will be clearer for me.

#### Reid Barton (Jun 28 2020 at 23:01):

It seems like you want to prove `0 ≠ 1`

for `fin 2`

. I think it will be better not to use type classes for this. (Especially since `matrix.one_val_ne`

doesn't want a type class argument anyways.)

Last updated: May 07 2021 at 21:10 UTC