Changes

Changeset 13068:1145c2ed8f6c by Dominique Unruh _unruh@ut.ee_:
Many changes to entry `Complex_Bounded_Operators`:<br>- Removed all use of deprecated `⟨.,.⟩` syntax for complex inner product. (Now: `∙⇩C`)<br>- Cosmetic changes and cleanup of some proofs<br>- Type class `one_dim` inherits from `complex_inner` now.<br>- Moved various theorems around between theories<br>- Added `[simp]` to: `Proj_partial_isometry`, `cadjoint_id`<br>- Removed theorems: `onorm_Inf_bound`, `norm_unit_sphere`<br>- Changed theorems: `of_complex_cblinfun_apply` (made into more general simp-rule), TODO orthospacething<br>- New definition: `rank1` (and lemmas about it)<br>- New theorems: `one_dim_iso_cblinfun_apply`, `vector_to_cblinfun_one_dim_iso`, `image_vector_to_cblinfun_adj`,<br>&nbsp; `image_vector_to_cblinfun_adj&#039;`, `sgn_cinner`, `orthocomplement_top`, `orthogonal_spaces_ccspan`, `norm_scaleC_sgn`,<br>&nbsp; `one_dim_ccsubspace_all_or_nothing`, `surj_isometry_is_unitary`<br>- Renamed `vector_to_cblinfun_cblinfun_apply` -&gt; `vector_to_cblinfun_cblinfun_compose` (also turned around and added `[simp]`),<br>&nbsp; `cancel_apply_Proj` -&gt; `Proj_fixes_image`, `range_is_clinear` -&gt; `range_is_csubspace`.<br>- Changed definition: `is_Proj` (logically equivalent by `Proj_range_closed`)<br><br>Fixed entry `Registers` due to the changes above.