## Stream: Is there code for X?

### Topic: Finite dimensional vector space over a finite field

#### Patrick Lutz (Jul 29 2020 at 19:30):

I suspect this is not in mathlib, but I would love to be wrong: does mathlib already have some theorem to the effect that a finite dimensional vector space over a finite field is finite?

I think so

#### Johan Commelin (Jul 29 2020 at 19:31):

vector_space.card_fintype?

#### Patrick Lutz (Jul 29 2020 at 19:33):

It looks to me like to use that theorem you have to already know that the vector space V is fintype. Or am I missing something?

#### Patrick Lutz (Jul 29 2020 at 19:35):

Oh wait, nevermind

#### Patrick Lutz (Jul 29 2020 at 19:35):

module.fintype_of_fintype takes care of it

#### Patrick Lutz (Jul 29 2020 at 22:49):

The reason I wanted to know this was to show that a finite extension of a finite field is finite. I proved it like this

import linear_algebra.finite_dimensional

open finite_dimensional

noncomputable lemma finite_of_findim_over_finite (F : Type*) (E : Type*) [field F] [field E]
[algebra F E] [fintype F] (hE : finite_dimensional F E) : fintype E :=
begin
set s := classical.some (exists_is_basis_finite F E) with hs,
have hs' := classical.some_spec (exists_is_basis_finite F E),
rw ← hs at hs',
cases hs' with s_basis s_finite,
have s_fintype : fintype ↥s := set.finite.fintype s_finite,
exact @module.fintype_of_fintype s F E (coe : s → E) _ _ _ s_fintype s_basis _,
end


but that feels a little gruesome. It feels like this should be something I can do in one line using module.fintype_of_fintype (and I believe it is, but I am just too inexperienced at Lean to see how). And does it really need to be uncomputable (I guess probably, since apparently module.fintype_of_fintype is)?

So, does anyone know how to make this proof totally trivial?

#### Aaron Anderson (Jul 30 2020 at 02:02):

This is what I did on the branch finite_fields_exist

variables {K : Type*} [field K] [fintype K]
variables {V : Type*} [add_comm_group V] [vector_space K V]

noncomputable def fintype_of_finite_dimensional [finite_dimensional K V] : fintype V :=
begin
have b := classical.some_spec (finite_dimensional.exists_is_basis_finset K V),
apply module.fintype_of_fintype b,
end


#### Patrick Lutz (Jul 30 2020 at 18:07):

@Aaron Anderson why did you make it a def rather than a lemma?

#### Patrick Lutz (Jul 30 2020 at 18:12):

Also, why does what you did work, but the following doesn't?

variables {K : Type*} [field K] [fintype K]
variables {V : Type*} [add_comm_group V] [vector_space K V]

noncomputable def fintype_of_finite_dimensional [finite_dimensional K V] : fintype V :=
begin
apply module.fintype_of_fintype (classical.some_spec (finite_dimensional.exists_is_basis_finset K V)),
end


#### Aaron Anderson (Jul 30 2020 at 18:12):

Because fintype is data, not a prop. I might be totally wrong about that convention though, let me check the library.

#### Aaron Anderson (Jul 30 2020 at 18:14):

Yeah, it looks like that’s standard.

#### Aaron Anderson (Jul 30 2020 at 18:15):

I don’t recall what error I got shortening it... I bet it can be golfed somehow, maybe even term mode

#### Patrick Lutz (Jul 30 2020 at 18:17):

This is the error

type mismatch at application
classical.some_spec (exists_is_basis_finset K V)
term
exists_is_basis_finset K V
has type
∃ (b : finset V), is_basis K coe
but is expected to have type
∃ (x : module ?m_1 ?m_2), is_basis ?m_1 ?m_6


#### Patrick Lutz (Jul 30 2020 at 18:17):

It's not able to do some type inference I guess

#### Patrick Lutz (Jul 30 2020 at 18:17):

but what I don't understand is why it could do it in your proof but not in this one

#### Patrick Lutz (Jul 30 2020 at 18:18):

And I ran into somewhat similar problems which is why my proof above is more complicated than I wanted

#### Markus Himmel (Jul 30 2020 at 18:20):

The following works:

noncomputable def fintype_of_finite_dimensional [finite_dimensional K V] : fintype V :=
module.fintype_of_fintype (classical.some_spec (finite_dimensional.exists_is_basis_finset K V) : _)


#### Patrick Lutz (Jul 30 2020 at 18:21):

@Markus Himmel interesting. So in your proof you're explicitly giving lean a hint about how to do type inference? Or am I still confused?

#### Markus Himmel (Jul 30 2020 at 18:22):

I actually have no idea but it might be related to this?

#### Patrick Lutz (Jul 30 2020 at 18:23):

So (t : _) is used to tell Lean to not be too aggressive about premature type inference?

#### Markus Himmel (Jul 30 2020 at 18:24):

I think it somehow says to Lean "do not look at what this is being applied to". By doing the have line first in the tactic proof, you achieve a similar effect.

#### Patrick Lutz (Jul 30 2020 at 18:25):

I'm not sure I understand what you mean by "do not look at what this is being applied to"

#### Patrick Lutz (Jul 30 2020 at 18:25):

Shouldn't looking at what it's being applied to help Lean to make the correct type inference?

#### Markus Himmel (Jul 30 2020 at 18:25):

I don't think I understand either, to be honest.

#### Kevin Buzzard (Jul 30 2020 at 18:28):

You're making type unification happen in a different order

#### Markus Himmel (Jul 30 2020 at 18:30):

Should it be obvious that the order matters?

#### Patrick Lutz (Jul 30 2020 at 18:31):

Kevin Buzzard said:

You're making type unification happen in a different order

Sure, I understand this. But why does (t : _) give me the order I want? I guess the basic issue is that I don't know what the usual order is or how this syntax changes it.

Last updated: May 17 2021 at 15:13 UTC