Skip to content

Commit

Permalink
chore: restore Type* in SpecificLimits/IsROrC.lean (#6515)
Browse files Browse the repository at this point in the history
This was accidentally changed in #6506.
  • Loading branch information
Ruben-VandeVelde authored and semorrison committed Aug 15, 2023
1 parent 726171c commit 61445f2
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Mathlib/Analysis/SpecificLimits/IsROrC.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ import Mathlib.Analysis.Complex.ReImTopology

open Set Algebra Filter

variable (π•œ : Type _) [IsROrC π•œ]
variable (π•œ : Type*) [IsROrC π•œ]

theorem IsROrC.tendsto_inverse_atTop_nhds_0_nat :
theorem IsROrC.tendsto_inverse_atTop_nhds_0_nat :
Tendsto (fun n : β„• => (n : π•œ)⁻¹) atTop (nhds 0) := by
convert tendsto_algebraMap_inverse_atTop_nhds_0_nat π•œ
simp

0 comments on commit 61445f2

Please sign in to comment.