Skip to content

Commit 8afd270

Browse files
committed
chore(Data/Fintype/WithTopBot): use to_dual (leanprover-community#37284)
1 parent abf93c0 commit 8afd270

1 file changed

Lines changed: 2 additions & 7 deletions

File tree

Mathlib/Data/Fintype/WithTopBot.lean

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -16,16 +16,11 @@ public import Mathlib.Order.TypeTags
1616

1717
variable {α : Type*}
1818

19+
@[to_dual]
1920
instance [Fintype α] : Fintype (WithTop α) :=
2021
instFintypeOption
2122

23+
@[to_dual]
2224
instance [Finite α] : Finite (WithTop α) :=
2325
have := Fintype.ofFinite α
2426
Finite.of_fintype _
25-
26-
instance [Fintype α] : Fintype (WithBot α) :=
27-
instFintypeOption
28-
29-
instance [Finite α] : Finite (WithBot α) :=
30-
have := Fintype.ofFinite α
31-
Finite.of_fintype _

0 commit comments

Comments
 (0)