Commit 2020-08-12 15:04 eb4b2a05
View on Github →feat(field_theory/algebraic_closure): algebraic closure (#3733)
instance : is_alg_closed (algebraic_closure k) :=
TODO: Show that any algebraic extension embeds into any algebraically closed extension (via Zorn's lemma).