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