Extend basic API about `DomMulAct`

This issue keeps track of missing basic API about DomMulAct.

Actions on functions

• action on α → β, see #5368;
• a MulDistribMulAction generates an action on A →* B, see #5368;
• a DistribMulAction generates an action on A →+ B, see #5368;
• an action on α that commutes with action of some other monoid N generates an action on α →[N] β, see #5378;
• a DistribMulAction on an R-module that commutes with scalar multiplications by c : R generates an action on R-linear maps from this module;
• a continuous action on X generates an action on C(X, Y);
• a measurable action on X generates an action on { f : X → Y // Measurable f }; we don't have a typeclass for measurable actions yet;
• a quasi measure preserving action on X generates an action on X →ₘ[μ] Y, see #5693;
• a measure preserving action generates an isometric action on MeasureTheory.Lp _ _ _ (done in a private branch).

Extra instances

For each action, we should add (at least) the following instances.

SMulCommClass

• if M and N act on α and the actions commute, then the actions of DoMulAct M and DomMulAct N commute.
• if M acts on the domain and N acts on the codomain, then the actions commute uncondiitonally

Distributivity

• If the codomain has a zero, then add ZeroSMulClass.
• If the maps also have pointwise Add instance, then add DistribSMul.
• If the maps form an AddZeroClass, then add DistribMulAction.
• If the maps have pointwise Mul instance, then add MulDistribMulAction.

Dynamical properties

• A function is invariant under the action if and only if it is constant on the orbits.
• In particular, if the action is (pre?)transitive, then the only invariant functions are constants.