DecidableEq on GaloisField

Stream: new members

[Matej Penciak]

I'm not sure if I'm barking up the wrong tree, but I feel like there should be an instance of DecidableEq (GaloisField p n). The fact that there isn't (and that I'm having a hard time defining it myself) suggests that I might have a misunderstanding of how DecidableEq works.

Intuitively I feel like it should follow from Finset.decidableEqPiFinset and the DecidableEq (ZMod p) instance (after all: GaloisField p nis a finite-rank ZMod p module).

Part of the reason I feel like I have a misunderstanding of DecidableEq is that it feels like any Fintype should have an instance of DecidableEq instance, and I've seen enough type declarations in Mathlib to see that [Fintype α] [DecidableEq α] is a common idiom.

To #xy the issue: I'm trying to do some probability theory on GaloisField p n, and I was hoping to use things like Finset.filter to define subsets where polynomial/matrix equations are satisfied.

[Coleton Kotch]

We have GaloisField.instFintype and decidablePiFintype which together give what I believe you are looking for.

[Daniel Weber]

I imagine the problem is that currently polynomials are mostly noncomputable

[Nico]

hello, thanks again for the help last time! I am back with more newbie questions :wave:
EDIT: nevermind reading the previous thread