Commit 2022-02-16 13:36 22fdf47e

chore(linear_algebra/affine_space/affine_map,topology/algebra/continuous_affine_map): generalized scalar instances (#11978) The main result here is that distrib_mul_actions are available on affine maps to a module, inherited from their codomain. This fixes a diamond in the int-action that was already present for int-affine maps, and prevents the new nat-action introducing a diamond. This also removes the requirement for R to be a topological_space in the scalar action for continuous_affine_map by using has_continuous_const_smul instead of has_continuous_smul.