findim = 1

Stream: Is there code for X?

[Thomas Browning]

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]

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]

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

[Anne Baanen]

Created #3720.

[Patrick Lutz]

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]

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]

(deleted)