Complex_Bounded_Operators: Various changes:
- Removed auxiliary constant the_riesz_rep_bilinear'
- Renamed constant the_riesz_rep_bilinear -> the_riesz_rep_sesqui and defined differently but equivalently
- Renamed constant bifunctional -> bidual_embedding (and renamed lemmas containing bifunctional accordingly)
- Renamed lemmas the_riesz_rep_bilinear_apply -> the_riesz_rep_sesqui_apply, cblinfun_extension_exists_norm -> cblinfun_extension_norm_bounded_dense
- New theorems: rank1_compose_left, rank1_compose_right, rank1_scaleC, rank1_uminus, rank1_uminus_iff, rank1_adj, rank1_adj_iff, bidual_embedding_surj, Cblinfun_comp_bounded_cbilinear, Cblinfun_comp_bounded_sesquilinear, bounded_clinear_0, bounded_antilinear_0, bounded_cbilinear_0, bounded_sesquilinear_0, bounded_cbilinear_apply_bounded_clinear, bounded_sesquilinear_apply_bounded_clinear, cblinfun_extension_exists_hilbert, trunc_ell2_reduces_norm, trunc_ell2_add, trunc_ell2_scaleC, bounded_clinear_trunc_ell2
- Theorem cblinfun_extension_exists_proj: Reformulated one assumption