mathlib

11d89a2f - chore(algebra/module): replace typeclass arguments with inferred arguments (#2444)

chore(algebra/module): replace typeclass arguments with inferred arguments (#2444) This doesn't change the explicit type signature of any functions, but makes some inferable typeclass arguments implicit. Beyond the potential performance improvement, my motivation for doing this was that in `monoid_algebra` we currently have two possible `module k (monoid_algebra k G)` instances: one directly from `monoid_algebra.module`, and another one via `restrict_scalars`. These are equal, but not definitionally. In another experimental branch, I couldn't even express the isomorphism between these module structures, because type inference was filling in the `monoid_algebra.module` instance in composition of linear maps, and then failing because one of the linear maps was actually using the other module structure... This change fixes this. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>