mathlib

639b66d9 - chore(topology/algebra/infinite_sum): correct argument explicitness (#18403)

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.