feat: DistribSMul R R instance for NonUnitalNonAssocSemiring R (#…

…10162)

Nonunital Nonassociative semirings act (in some sense) on themselves by multiplication, and this multiplication satisfies the requirements of the `DistribSMul` class.  This is part of a refactor of HahnSeries that includes having `HahnSeries Γ R` act on `HahnSeries Γ V` for `V` an `R`-module.

I'm not sure about the best file for this instance.  `#find_home!` suggested `Mathlib.Algebra.SMulWithZero`, but it looks a bit strange there.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/SMulWithZero.lean

@@ -229,3 +229,8 @@ def smulMonoidWithZeroHom {α β : Type*} [MonoidWithZero α] [MulZeroOneClass 
   { smulMonoidHom with map_zero' := smul_zero _ }
 #align smul_monoid_with_zero_hom smulMonoidWithZeroHom
 #align smul_monoid_with_zero_hom_apply smulMonoidWithZeroHom_apply
+
+-- This instance seems a bit incongruous in this file, but `#find_home!` told me to put it here.
+instance NonUnitalNonAssocSemiring.toDistribSMul [NonUnitalNonAssocSemiring R] :
+    DistribSMul R R where
+  smul_add := mul_add