complex.is_alg_closed

Stream: general

[Scott Morrison]

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]

yup, good idea

[Scott Morrison]

#7344