nonzero (fin n.succ.succ)

Stream: Is there code for X?

[Yakov Pechersky]

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]

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]

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]

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]

Or maybe I misunderstood, do you want matrices valued in fin n or with fin n as the index set?

[Yakov Pechersky]

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]

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]

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.)