## 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:

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: May 18 2021 at 08:14 UTC