mathlib
3ab512ea - Delete unnecessary `coe_to_fun`
Commit
View On GitHub
Commit
4 years ago
Delete unnecessary `coe_to_fun`
Author
Vierkantor Vierkantor
Parents
aae564ad
FAQ Terms Privacy Refunds Impressum
Loading