Skip to content

Commit

Permalink
doc(Analysis/RCLike/Basic): correct link in documentation (#18343)
Browse files Browse the repository at this point in the history
  • Loading branch information
Command-Master committed Oct 28, 2024
1 parent 91c4956 commit 97a2bd1
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Analysis/RCLike/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 97a2bd1

Please sign in to comment.