mathlib

f1397dc1 - feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand transform is a bijective isometry for C⋆-algebras over ℂ (#16488)

feat(analysis/normed_space/star/gelfand_duality): Show the Gelfand transform is a bijective isometry for C⋆-algebras over ℂ (#16488) - [x] depends on: #16451 - [x] depends on: #16438 - [x] depends on: #16368 - [x] depends on: #16303 - [x] depends on: #16446 - [x] depends on: #16448