## Stream: maths

### Topic: is_integral_of_finite_extension

#### Jack J Garzella (Jun 23 2020 at 20:03):

I am attempting to prove the following lemma:

lemma is_integral_of_finite_extension {F : Type u} {L : Type v}
[field F] [field L] [algebra F L] [finite_dimensional F L]
(x : L) : is_integral F x :=
sorry


I thought the best approach would be to use the is_integral_of_mem_of_fg lemma, combined with iff_fg in finite_dimensional.lean. However, I have been unable to get lean to translate between these three objects:

• ⊤ : submodule F L
• ⊤ : subalgebra F L
• L itself

Put succinctly, iff_fg is written in terms of ⊤ : submodule F L, and is_integral_of_mem_of_fg requires a subalgebra type, while my mental model wants to use L.
I see three possible approaches:

1. write everything in terms of ⊤ : subalgebra F L.
But doing this would require a term of type (⊤ : subalgebra F L).to_submodule = (⊤ : submodule F L), which I don't know how to do.

2. write everthing in terms of ⊤ : submodule F L.
In this case, I just don't know how to convert a submodule into a subalgebra in the presence of multiplication.

3. write everthing in terms of L.
This seems to require coercing L to be a submodule and proving that it is equal to ⊤ : submodule F L.

Any advice on which direction I should go?

#### Kevin Buzzard (Jun 23 2020 at 20:17):

@Kenny Lau did you already prove this?

I don't think so

#### Kevin Buzzard (Jun 23 2020 at 20:18):

It's some noetherian thing

#### Chris Hughes (Jun 23 2020 at 20:30):

I recall seeing this recently in a PR.

#3096

#### Jack J Garzella (Jun 23 2020 at 23:39):

#3096 works great--thanks!

Last updated: May 14 2021 at 18:28 UTC