chore(analysis/complex/basic): golf some proofs (#17259)
This also generalizes `add_monoid_hom.map_real_smul` to `add_monoid_hom_class` and removes the namespace to match `map_rat_smul`.
The `ring_hom_eq_of_real_of_continuous` lemma is new, but a trivial consequence of existing lemmas.
