mathlib

f12b3d91 - feat(topology/algebra): weaken typeclasses to only require `has_continuous_const_smul` (#11995)

feat(topology/algebra): weaken typeclasses to only require `has_continuous_const_smul` (#11995) This changes all the continuity-based `const_smul` lemmas to only require `has_continuous_const_smul` rather than `has_continuous_smul`. It does not attempt to propagate the changes out of this file. Four new instances are added in `const_mul_action.lean` for `has_continuous_const_smul`: `mul_opposite`, `prod`, `pi`, and `units`; all copied from the corresponding `has_continuous_smul` instance in `mul_action.lean`. Presumably these lemmas existed before this typeclass did. At any rate, the connection was less obvious until the rename a few days ago in #11940. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>