Commit 2023-02-08 12:29 2407f3b1

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.