Commit 2023-02-09 08:59 639b66d9

chore(topology/algebra/infinite_sum): correct argument explicitness (#18403) It is quite annoying to use the current const_smul and smul_const, because Lean often can't even infer the type of this implicit argument. There was one existing place in mathlib where this became really painful (the @ in the diff), and there are a couple more in one of my branches.