Skip to content

Commit cd8f5ab

Browse files
feat: port Data.Fintype.Card (#1668)
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
1 parent 38551b8 commit cd8f5ab

File tree

2 files changed

+1241
-0
lines changed

2 files changed

+1241
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -254,6 +254,7 @@ import Mathlib.Data.Finset.Prod
254254
import Mathlib.Data.Finset.Sigma
255255
import Mathlib.Data.Finset.Sum
256256
import Mathlib.Data.Fintype.Basic
257+
import Mathlib.Data.Fintype.Card
257258
import Mathlib.Data.Fintype.List
258259
import Mathlib.Data.Fintype.Pi
259260
import Mathlib.Data.Fintype.Sigma

0 commit comments

Comments
 (0)