mathlib3

be75005c - fix(linear_algebra/tensor_product): Remove the priorities from the module structure (#5667)

fix(linear_algebra/tensor_product): Remove the priorities from the module structure (#5667) These were added originally so that `semimodule'` was lower priority than `semimodule`, as the `semimodule'` instance took too long to resolve. However, this happens automatically anyway, since the former appears before the latter - the simple existence of the `semimodule` shortcut instances was enough to solve the long typeclass-resolution paths, their priority was a red herring. The only effect of these attributes was to cause these instances to not take priority over `add_comm_monoid.nat_semimodule`, which was neither intended nor desirable.