Commit 2023-08-16 09:33 38c07226

refactor(Data/Matrix): Eliminate ⬝ notation in favor of HMul (#6487) The main difficulty here is that * has a slightly difference precedence to ⬝. notably around smul and neg. The other annoyance is that ↑U ⬝ A ⬝ ↑U⁻¹ : Matrix m m 𝔸 now has to be written U.val * A * (U⁻¹).val in order to typecheck. A downside of this change to consider: if you have a goal of A * (B * C) = (A * B) * C, mul_assoc now gives the illusion of matching, when in fact Matrix.mul_assoc is needed. Previously the distinct symbol made it easy to avoid this mistake. On the flipside, there is now no need to rewrite by Matrix.mul_eq_mul all the time (indeed, the lemma is now removed).