algebraically closed fields

Stream: maths

[Apurva Nakade]

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]

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]

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

[Apurva Nakade]

I see, thanks!

[Kevin Buzzard]

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]

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

[Apurva Nakade]

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]

Induct on degree :-)

[Aaron Anderson]

We do have field_theory/splitting_field

[Aaron Anderson]

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