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> `image_vector_to_cblinfun_adj'`, `sgn_cinner`, `orthocomplement_top`, `orthogonal_spaces_ccspan`, `norm_scaleC_sgn`,<br> `one_dim_ccsubspace_all_or_nothing`, `surj_isometry_is_unitary`<br>- Renamed `vector_to_cblinfun_cblinfun_apply` -> `vector_to_cblinfun_cblinfun_compose` (also turned around and added `[simp]`),<br> `cancel_apply_Proj` -> `Proj_fixes_image`, `range_is_clinear` -> `range_is_csubspace`.<br>- Changed definition: `is_Proj` (logically equivalent by `Proj_range_closed`)<br><br>Fixed entry `Registers` due to the changes above.