Zulip Chat Archive

Stream: Is there code for X?

Topic: nonzero (fin n.succ.succ)


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

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

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

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

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

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

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

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