feat(topology/algebra/star): continuity of `star` (#13855)
This adds the obvious instances for `pi`, `prod`, `units`, `mul_opposite`, `real`, `complex`, `is_R_or_C`, and `matrix`.
We already had a `continuous_star` lemma, but it had stronger typeclass assumptions.
This resolves multiple TODO comments.
Co-authored-by: Johan Commelin <johan@commelin.net>
