Add typeclasses for smooth `(· • ·)`

[urkud]

• Add a typeclass for ∀ c, Smooth I I (c • ·).
• Add a typeclass for Smooth (I.prod J) J (Function.uncurry (· • ·))

See ContinuousConstSMul and ContinuousSMul for example of API.

[grunweg]

#38565 adds ContMDiffSMul (#38357 adds a ContDiff version).
As discussed on zulip, it's unclear whether a ContMDiffConstSMul typeclass would be useful in practice. At the moment,

• I know of no application where this would come in handy, and
• in many cases (e.g., continuous action by a finite-dimensional Lie group on a finite-dimensional manifold), the definition is equivalent to the current definition.

I propose closing this issue once #38565 has been merged.