From 069f950f24fa6adde20ab94181ca4ea9d198dc0a Mon Sep 17 00:00:00 2001 From: Daniel Weber Date: Sat, 14 Sep 2024 06:37:26 +0300 Subject: [PATCH] Move --- Mathlib.lean | 2 +- Mathlib/Analysis/{Cauchy.lean => CauchyBound.lean} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename Mathlib/Analysis/{Cauchy.lean => CauchyBound.lean} (100%) diff --git a/Mathlib.lean b/Mathlib.lean index ea8315d1de0f7..b79a7fa8c119a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1025,7 +1025,7 @@ import Mathlib.Analysis.Calculus.SmoothSeries import Mathlib.Analysis.Calculus.TangentCone import Mathlib.Analysis.Calculus.Taylor import Mathlib.Analysis.Calculus.UniformLimitsDeriv -import Mathlib.Analysis.Cauchy +import Mathlib.Analysis.CauchyBound import Mathlib.Analysis.Complex.AbelLimit import Mathlib.Analysis.Complex.AbsMax import Mathlib.Analysis.Complex.Angle diff --git a/Mathlib/Analysis/Cauchy.lean b/Mathlib/Analysis/CauchyBound.lean similarity index 100% rename from Mathlib/Analysis/Cauchy.lean rename to Mathlib/Analysis/CauchyBound.lean