Zulip Chat Archive

Stream: general

Topic: complex.is_alg_closed


Scott Morrison (Apr 23 2021 at 12:07):

Could I move complex.is_alg_closed out of field_theory.algebraic_closure into its own file under analysis.complex? Having it there puts a gigantic amount of stuff (measure spaces, formal multilinear series, normed spaces, oh me) into the import hierarchy under linear_algebra.eigenspace, which can otherwise be fairly elementary.

Johan Commelin (Apr 23 2021 at 12:07):

yup, good idea

Scott Morrison (Apr 23 2021 at 12:15):

#7344


Last updated: Dec 20 2023 at 11:08 UTC