mathlib3

6abfb1d7 - feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem (#12787)

feat(analysis/normed_space/spectrum): Prove the Gelfand-Mazur theorem (#12787) **Gelfand-Mazur theorem** For a complex Banach division algebra, the natural `algebra_map ℂ A` is an algebra isomorphism whose inverse is given by selecting the (unique) element of `spectrum ℂ a`. - [x] depends on: #12132 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>