feat(analysis/complex/basic): lemmas about tsum (#18376)
This adds lemmas about the four "basis" complex operations: `re`, `im`, `of_real` (coercion), and `conj`.
These all follow trivially from the API for continuous linear morphisms, but using those results directly gives syntacticly different terms that don't work in rewrites. Similarly, the conj lemmas follow trivially from the results about `star`, but `conj` (aka `star_ring_end`) is not a syntactic match for `star`.
This proves all the results for `is_R_or_C` (including a more general version of `has_sum_iff`), then copies across the results to `complex` for convenience.
