mathlib

48085f14 - chore(algebra/quaternion): generalize the algebra instance (#18382)

chore(algebra/quaternion): generalize the algebra instance (#18382) To prevent this generalization forming diamonds, we have to now populate the `nsmul`, `zsmul`, and `qsmul` fields. I use this in another PR to talk about the `R` algebra structure of `quaternion (dual_number R)`. Even without that motivation, this change means that the existing `smul` lemmas now apply to `nsmul`, `zsmul`, and `rat_smul` where previously they did not.