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).

Estimated changes