Commit 2022-10-31 09:21 7c9a3b4b
View on Github →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.