match_pattern attribute on Mul.mul

Stream: lean4

[Lukas Miaskiwskyi]

Thought this was worth asking here since it's about a file in Init. When porting Algebra.Free (see PR mathlib4#1353), the line attribute [match_pattern] Mul.mul causes the error invalid attribute 'match_pattern', declaration is in an imported module. This apparently worked in lean 3, but I'm guessing it does not like adding attributes to declarations in other files anymore. Would it be a desirable fix to add this attribute to Mul.mul (or HMul.hmul?) in Init.Prelude? Or should we try to avoid that and find a local solution?

EDIT: See also the discussion in this thread.