Commit 2022-02-15 08:27 f12b3d91

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.