## Stream: Is there code for X?

### Topic: findim = 1

#### Thomas Browning (Aug 07 2020 at 06:42):

If F is a subfield of E and findim F E = 1 (or dim F E = 1), is there something in mathlib to allow me to conclude that F is all of E (F = ⊤)?

#### Anne Baanen (Aug 07 2020 at 09:02):

I do not believe so at the moment. I'm working on a PR that would allow you to conclude this from the fact {1} is a linearly independent set.

#### Kevin Buzzard (Aug 07 2020 at 09:59):

Again, one has to be clear here whether F is a term of type subfield E or whether F is a type and there is an algebra F E instance

Created #3720.

#### Patrick Lutz (Aug 07 2020 at 17:16):

This is really great, it's just the sort of lemma we need. But one thing is confusing me. I tried copying and pasting the code from your PR into our codebase and Lean tells me that the lemma findim_lt uses sorry, but when I look at the code there are no sorry's visible nor any unsolved goals at the end of the proof. Does anyone have any idea what's going on?

#### Patrick Lutz (Aug 07 2020 at 17:18):

Okay, nevermind. @Thomas Browning has pointed out to me that I left out one of the variable declarations, which is what was causing the problem.

#### Thomas Browning (Aug 07 2020 at 17:19):

(deleted)

Last updated: May 07 2021 at 22:14 UTC