n-th degree closed field

Stream: Is there code for X?

[Violeta Hernández]

Do we happen to have a typeclass/any theorems for fields where polynomials of degree ≤ n have roots?

[Violeta Hernández]

These come up quite a lot in the context of nimbers

[Violeta Hernández]

For context, we want to formalize the following argument:
image.png

[Scott Carnahan]

You may have accounted for this already, but I would like to emphasize for other readers that the condition in that passage is “not irreducible” rather than “has a root”.

[Violeta Hernández]

Ah, that's a fair point.

[Violeta Hernández]

Well, that's already an argument against having such a typeclass: it's too strong for at least one of the results we want to prove about it!