mathlib
a84a80d5
- fix(topology/algebra/infinite_sum): add missing decidable arguments (#5993)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
fix(topology/algebra/infinite_sum): add missing decidable arguments (#5993) These decidable instances were being inferred as classical instances, which meant these lemmas would not match other instances.
Author
eric-wieser
Parents
64283ce9
Loading