Commit 2022-01-03 10:32 a813cf5c

chore(algebra/algebra/spectrum): move exists_spectrum_of_is_alg_closed_of_finite_dimensional (#10919) Move a lemma from field_theory/is_alg_closed/basic into algebra/algebra/spectrum which belongs in this relatively new file. Also, rename (now in spectrum namespace) and refactor it slightly; and update the two references to it accordingly.

• depends on: #10783