From 6ec755312bc5afd113cd584e36ec9372c520a2db Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sat, 13 Dec 2025 07:15:12 +0100
Subject: [PATCH] Update Basic.lean

---
 Aristotle/Basic.lean | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean
index 0e1b0e8..331fcc7 100644
--- a/Aristotle/Basic.lean
+++ b/Aristotle/Basic.lean
@@ -1,8 +1,15 @@
 import Mathlib
 
-variable
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
 
-lemma MeromorphicAt.comp {x : ℝ} {f : ℂ → E} {g : ℝ → ℂ}
-    (hf : MeromorphicAt f (g x)) (hg : AnalyticAt ℝ g x) : MeromorphicAt (f ∘ g) x := by
+theorem intervalIntegrable_iff_intervalIntegrable_smul
+    {E : Type*} [NormedAddCommGroup E]
+    {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
+    {R : Type*} [NormedAddCommGroup R] [SMulZeroClass R E] [IsBoundedSMul R E]
+    {f : ℝ → E} {r : R} (hr : r ≠ 0) :
+    IntervalIntegrable f μ a b ↔ IntervalIntegrable (r • f) μ a b := by
+  sorry
+
+theorem IntervalIntegrable.abs'
+    {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} (hf : Measurable f) :
+    IntervalIntegrable f μ a b ↔  IntervalIntegrable (fun x => |f x|) μ a b := by
   sorry