Algebraically closed subfield

Stream: Is there code for X?

[Violeta Hernández]

Just making sure I'm not missing something, we don't have a type for algebraically closed subfields the way we do for docs#Subfield, do we?

[Violeta Hernández]

Actually I think I can use docs#algebraicClosure for what I want so nvm

[Violeta Hernández]

Nevermind, I think I do want this. I want to prove some theorems about algebraically closed subfields of a larger algebraically closed type R, and it's kind of annoying that the simplest way to write down that a given subfield x is algebraically closed is via algebraicClosure x R = x

[Violeta Hernández]

Maybe what I want instead is a predicate Subfield.IsAlgClosed? And then I can show that's equivalent to all the different characterizations.

[Violeta Hernández]

#34646