Zulip Chat Archive

Stream: Is there code for X?

Topic: findim = 1


view this post on Zulip 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 = ⊤)?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Anne Baanen (Aug 07 2020 at 11:27):

Created #3720.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Thomas Browning (Aug 07 2020 at 17:19):

(deleted)


Last updated: May 07 2021 at 22:14 UTC