mathlib
5a5d2909
- fix(data/fintype/basic): move card_subtype_mono into the fintype namespace (#15185)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
fix(data/fintype/basic): move card_subtype_mono into the fintype namespace (#15185)
Author
linesthatinterlace
Parents
1937dff0
Loading