Commit 2021-02-01 19:15 a84a80d5
View on Github →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.