Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Lebesgue_Measure.thy
changeset 78656 4da1e18a9633
parent 76786 50672d2d78db 
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sat Sep 09 17:18:52 2023 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Sat Sep 09 19:26:08 2023 +0100
@@ -1092,11 +1092,6 @@
   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"
-  using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp
-
 lemma lborel_has_bochner_integral_real_affine_iff:
   fixes x :: "'a :: {banach, second_countable_topology}"
   shows "c \<noteq> 0 \<Longrightarrow>
isabelle