From 97a2bd10ed6b19fba3f98a628201ad73ddaa1306 Mon Sep 17 00:00:00 2001 From: Daniel Weber Date: Mon, 28 Oct 2024 16:16:03 +0000 Subject: [PATCH] doc(Analysis/RCLike/Basic): correct link in documentation (#18343) --- Mathlib/Analysis/RCLike/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean index 039e769c1b674..0600c19d1b79e 100644 --- a/Mathlib/Analysis/RCLike/Basic.lean +++ b/Mathlib/Analysis/RCLike/Basic.lean @@ -39,7 +39,7 @@ in `Mathlib/Data/Nat/Cast/Defs.lean`. See also Note [coercion into rings] for mo In addition, several lemmas need to be set at priority 900 to make sure that they do not override their counterparts in `Mathlib/Analysis/Complex/Basic.lean` (which causes linter errors). -A few lemmas requiring heavier imports are in `Mathlib/Data/RCLike/Lemmas.lean`. +A few lemmas requiring heavier imports are in `Mathlib/Analysis/RCLike/Lemmas.lean`. -/ open Fintype