[Merged by Bors] - feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand transform is a bijective isometry for C⋆-algebras over ℂ

[j-loreaux]

• depends on: [Merged by Bors] - feat(topology/algebra/module/character_space, analysis/normed_space/star/spectrum): define the Gelfand transform as an alg_hom #16451
• depends on: [Merged by Bors] - feat(data/complex/module): define real_part and imaginary_part #16438
• depends on: [Merged by Bors] - feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete #16368
• depends on: [Merged by Bors] - feat(analysis/normed_space/units): maximal ideals in complete normed rings are closed #16303
• depends on: [Merged by Bors] - feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals #16446
• depends on: [Merged by Bors] - refactor(analysis/normed_space/spectrum): generalize Gelfand-Mazur away from normed_division_ring #16448

---

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(topology/algebra/module/character_space, analysis/normed_space/star/spectrum): define the Gelfand transform as an alg_hom #16451
• [Merged by Bors] - feat(data/complex/module): define real_part and imaginary_part #16438
• [Merged by Bors] - feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete #16368
• [Merged by Bors] - feat(analysis/normed_space/units): maximal ideals in complete normed rings are closed #16303
• [Merged by Bors] - feat(analysis/normed/group/quotient): transfer norm structures on quotients of groups to quotients of modules by submodules and of rings by ideals #16446
• [Merged by Bors] - refactor(analysis/normed_space/spectrum): generalize Gelfand-Mazur away from normed_division_ring #16448
  By Dependent Issues (🤖). Happy coding!

[dupuisf]

Very nice! How about also adding gelfand_transform_bijective (or even just replacing gelfand_transform_surjective by this)?

bors d+

[bors]

✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests