--- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Dec 04 23:10:52 2017 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Tue Dec 05 12:14:36 2017 +0100
@@ -819,6 +819,11 @@
unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult prod_nonneg)
qed
+lemma lebesgue_real_scale:
+ assumes "c \<noteq> 0"
+ shows "lebesgue = density (distr lebesgue lebesgue (\<lambda>x. c * x)) (\<lambda>x. ennreal \<bar>c\<bar>)"
+ using assms by (subst lebesgue_affine_euclidean[of "\<lambda>_. c" 0]) simp_all
+
lemma divideR_right:
fixes x y :: "'a::real_normed_vector"
shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"