a noncomputable def of Fintype

Stream: mathlib4

[Yongle Hu]

I found that FiniteDimensional.fintypeOfFintype is a noncomputable def of Fintype. My understanding is that Fintype should only be used in cases where it is computable in the reduction or #eval sense, so this definition might be bad. Should we deprecate this definition?

[Yongle Hu]

For example, FiniteDimensional.fintypeOfFintype is used to prove that GaloisField is Fintype, but we cannot calculate the number of elements in GaloisField 3 3 using #eval.

import Mathlib

#eval Fintype.card (GaloisField 3 3)

[Eric Wieser]

It's definitely tempting to change it to Finite

[Eric Wieser]

But I think that Fintype.card (GaloisField 3 3) should remain legal, and the fact it doesn't #eval is unfortunate but not a reason to disable the Fintype instance.

[Edward van de Meent]

The fact that it doesn't fin_cases might be?

[Ruben Van de Velde]

Why not Nat.card?

[Yongle Hu]

I think it is better to replace Fintype.card with Nat.card in the theorems about GaloisField (for example, GaloisField.algEquivGaloisField).

[Eric Wieser]

Edward van de Meent said:

The fact that it doesn't fin_cases might be?

fin_cases behaves poorly with many types

[Kyle Miller]

I think it makes sense turning these into theorems that prove Finite.

At least FiniteDimensional.fintypeOfFintype isn't an instance. Noncomputable fintype instances are bad because they can cause things to become noncomputable. The point of Fintype over Finite is that you can (at least in theory) compute with it.

I'd strongly suggested turning the noncomputable GaloisField Fintype instance into a Finite one because of this. If somehow a Fintype instance is still useful, at least it should be scoped.

[Yongle Hu]

I find it is a little difficult to replace Fintype.card with Nat.card in the theorems related to GaloisField, because many theorems used in the proof (such as FiniteField.roots_X_pow_card_sub_X, Polynomial.card_rootSet_eq_natDegree, Module.card_fintype) only have versions for Fintype.card and do not have versions for Nat.card.

[Kyle Miller]

Can you use something like docs#Fintype.ofFinite to connect up the theories? You can do things like have := Fintype.ofFinite ty to temporarily introduce Fintype instances.

[Yongle Hu]

I think I can temporarily write a private instance of Fintype (GaloisField p n), and then use Nat.card_eq_fintype_card to relate Nat.card and Fintype.card. But I think it may be necessary to add Nat.card versions of those theorems in the future.

[Yongle Hu]

Opened #18106.