Zulip Chat Archive

Stream: maths

Topic: algebraically closed fields


view this post on Zulip Apurva Nakade (Jul 18 2020 at 14:24):

It seems like we don't have the definition of an algebraically closed field (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Undergraduate.20math.20list/near/199401708) even though we do have the fundamental theorem of algebra for complex numbers.
Is there some fundamental reason why this definition does not exist in mathlib?

view this post on Zulip Alex J. Best (Jul 18 2020 at 14:30):

The reason is that nobody finished proving algebraic closures exist yet. That doesn't preclude the definition from being added, but adding a definition without surrounding theory you can realise later that you need the definition to change for the theory to work best.

view this post on Zulip Johan Commelin (Jul 18 2020 at 14:30):

nope, merely laziness + the fact that we only have so many fingers typing code :wink: :grinning_face_with_smiling_eyes:

view this post on Zulip Apurva Nakade (Jul 18 2020 at 16:05):

I see, thanks!

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 16:19):

If you want to make a local definition then you might want to take the precise statement which Chris proved about the complex numbers and use that as the definition of alg closed. I find it a bit annoying that we don't have this definition.

view this post on Zulip Apurva Nakade (Jul 18 2020 at 16:24):

Will do! Very conveniently exists_root is exactly the property I need :D

view this post on Zulip Apurva Nakade (Jul 18 2020 at 16:29):

Scratch that. I actually need that a polynomial can be written as a product of linear terms. But I'll hopefully be able to figure that out. Thanks!

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 16:46):

Induct on degree :-)

view this post on Zulip Aaron Anderson (Jul 18 2020 at 17:48):

We do have field_theory/splitting_field

view this post on Zulip Aaron Anderson (Jul 18 2020 at 17:48):

Which does have some results about writing a polynomial as a product of linear terms


Last updated: May 18 2021 at 08:14 UTC