naming of `integralM`

[affeldt-aist]

analysis/theories/lebesgue_integral.v

Lines 2026 to 2027 in 46f7a6c

	Lemma ge0_integralM (k : \bar R) : (forall x, D x -> 0 <= f x) ->
	0 <= k -> \int[mu]_(x in D) (k * f x)%E = k * \int[mu]_(x in D) (f x).

shouldn't this be named integral_distrr on the model of big_distrr?

[CohenCyril]

big_distrr does not presume the operators at play and is about distributivity, here they are defined and this is not distributivity (addition/integral does not distributes over multiplication) but (nonnegative) scalability. However just M suggest we are taking the product of two functions. Hence I would go for Z or Zl instead

[affeldt-aist]

or maybe rM and Mr ?