mathlib

f7038c24 - feat(analysis/inner_product_space/adjoint): show that continuous linear maps on a Hilbert space form a C*-algebra (#10837)

feat(analysis/inner_product_space/adjoint): show that continuous linear maps on a Hilbert space form a C*-algebra (#10837) This PR puts a `cstar_ring` instance on `E →L[𝕜] E`, thereby showing that it forms a C*-algebra. - [x] depends on: #10825 [which defines the adjoint] Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>