# Zulip Chat Archive

## 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
```

Might help you understand what's going wrong

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

(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