mathlib

ba6b1422 - refactor(analysis/normed_space/spectrum): generalize Gelfand-Mazur away from `normed_division_ring` (#16448)

refactor(analysis/normed_space/spectrum): generalize Gelfand-Mazur away from `normed_division_ring` (#16448) This generalizes the Gelfand-Mazur theorem so that it does not require the hypothesis that the algebra is a `normed_division_ring`, but instead is only a `normed_ring` in which the nonzero elements are precisely the units. This is important for applications of the Gelfand-Mazur theorem in which one may not be able to prove *a priori* that `∥a * b∥ = ∥a∥ * ∥b∥`, even though it may follow *a posteriori* from the Gelfand-Mazur isomorphism. An explicit example of this is the quotient of a complex Banach algebra by a maximal ideal, which is the use case that prompted this change.