## Stream: new members

### Topic: Bottom subalgebra over fields is finite-dimensional

#### Sebastian Monnet (Dec 19 2021 at 10:48):

Let $L/K$ be a field extension. I'm trying to show that ⊥ is finite-dimensional over $K$. Here's my attempt:

import field_theory.galois

lemma fin_dim_bot (K L : Type*) [field K] [field L] [algebra K L] : finite_dimensional K (⊥ : intermediate_field K L) :=
begin
exact finite_dimensional_of_dim_eq_one (subalgebra.dim_bot),
end


The problem is that the subalgebra.dim_bot has type module.rank ?m_1 ↥⊥ = 1, and I need it to have type module.rank K ↥⊥ = 1. I've seen this ?m_1 notation before, and I think it means that the result is true for any type, but I don't know how to insert the type I want (namely K). I've tried things like subalgebra.dim_bot K and subalgebra.dim_bot K L, but none of it has worked.

I'd appreciate any guidance or explanation of what I need to do.

#### Eric Wieser (Dec 19 2021 at 10:54):

set_option pp.implicit true will give a clearer message

#### Eric Wieser (Dec 19 2021 at 10:56):

begin
refine finite_dimensional_of_dim_eq_one _,
convert subalgebra.dim_bot,
sorry
end


(untested)

#### Sebastian Monnet (Dec 19 2021 at 11:14):

Hmm, well I solved the problem by using your refine tactic and then just whacking it with simp. I still have no idea what the original problem was, or what simp actually did in this instance.

Using convert subalgebra.dim_bot creates six goals, some of which are really weird. The first one is module.rank K ↥⊥ = module.rank ?m_1 ↥⊥, which seems to be exactly the same as the original problem, since I don't know what this ?m_1 is or how to interact with it.

#### Eric Wieser (Dec 19 2021 at 11:28):

?m_1 means " I can't work out what to put here"

#### Eric Wieser (Dec 19 2021 at 11:29):

Probably because the bits you can't see without pp.implicit true don't match at all

#### Eric Wieser (Dec 19 2021 at 11:29):

simp? will tell you what simp did

#### Stuart Presnell (Dec 19 2021 at 11:58):

This might be a way to see more clearly what's going on:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Tips.20and.20tricks/near/265410441

Last updated: Dec 20 2023 at 11:08 UTC