Commit 2021-12-24 23:09 f7038c24

View on Github →

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.

depends on: #10825 [which defines the adjoint]

Estimated changes

Modified src/analysis/inner_product_space/adjoint.lean

added theorem continuous_linear_map.apply_norm_eq_sqrt_inner_adjoint_left

added theorem continuous_linear_map.apply_norm_eq_sqrt_inner_adjoint_right

added theorem continuous_linear_map.apply_norm_sq_eq_inner_adjoint_left

added theorem continuous_linear_map.apply_norm_sq_eq_inner_adjoint_right

added theorem continuous_linear_map.star_eq_adjoint

Modified src/analysis/inner_product_space/basic.lean

added theorem re_inner_le_norm