Zulip Chat Archive

Stream: maths

Topic: algebraically closed fields


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?

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.

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:

Apurva Nakade (Jul 18 2020 at 16:05):

I see, thanks!

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.

Apurva Nakade (Jul 18 2020 at 16:24):

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

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!

Kevin Buzzard (Jul 18 2020 at 16:46):

Induct on degree :-)

Aaron Anderson (Jul 18 2020 at 17:48):

We do have field_theory/splitting_field

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: Dec 20 2023 at 11:08 UTC