[Merged by Bors] - refactor(Data/Matrix): Eliminate ⬝ notation in favor of HMul
#6487
Conversation
eric-wieser
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
merge-conflict
eric-wieser
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
eric-wieser
removed
the
merge-conflict
There was a problem hiding this comment.
To help reviewing, I marked every single line which has a non-trivial change with a comment (marking this). They might not require attention.
"trivial" changes are
⬝to*in the context of matrices- removing
rw [Matrix.mul_eq_mul] - prec order
-A ⬝ Bto-(A * B)
Most other comments are about docstrings that need to be adapted
Mathlib/Algebra/Lie/SkewAdjoint.lean
Outdated
| -- TODO(mathlib4#6487): fix elaboration so annotation on `A` isn't needed | ||
| theorem skewAdjointMatricesLieSubalgebraEquiv_apply (P : Matrix n n R) (h : Invertible P) | ||
| (A : skewAdjointMatricesLieSubalgebra J) : | ||
| ↑(skewAdjointMatricesLieSubalgebraEquiv J P h A) = P⁻¹ ⬝ ↑A ⬝ P := by | ||
| ↑(skewAdjointMatricesLieSubalgebraEquiv J P h A) = P⁻¹ * (A : Matrix n n R) * P := by |
| -- TODO(mathlib4#6487): fix elaboration so `val` isn't needed | ||
| theorem exp_units_conj' (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸) : | ||
| exp 𝕂 (↑U⁻¹ ⬝ A ⬝ U : Matrix m m 𝔸) = ↑U⁻¹ ⬝ exp 𝕂 A ⬝ U := | ||
| exp 𝕂 ((U⁻¹).val * A * U.val) = (U⁻¹).val * exp 𝕂 A * U.val := |
| -- TODO(mathlib4#6487): fix elaboration so `val` isn't needed | ||
| nonrec theorem exp_units_conj (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸) : | ||
| exp 𝕂 (↑U ⬝ A ⬝ ↑U⁻¹ : Matrix m m 𝔸) = ↑U ⬝ exp 𝕂 A ⬝ ↑U⁻¹ := by | ||
| exp 𝕂 (U.val * A * (U⁻¹).val) = U.val * exp 𝕂 A * (U⁻¹).val := by |
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
|
I've hopefully addressed all the bad docstrings now. |
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
Thank you @eric-wieser for doing all this and @joneugster for the very helpful review. I note some minor points remain to be fixed after merging master but I've looked over the diffs and I think this leaves us much better off. In particular I'm happy to see no increase in bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
I think the increases is just incredibly small; in the previous revision, adding or removing |
|
bors merge |
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).
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
⬝ notation in favor of HMul⬝ notation in favor of HMul
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).
The main difficulty here is that
*has a slightly difference precedence to⬝. notably aroundsmulandneg.The other annoyance is that
↑U ⬝ A ⬝ ↑U⁻¹ : Matrix m m 𝔸now has to be writtenU.val * A * (U⁻¹).valin order to typecheck.A downside of this change to consider: if you have a goal of
A * (B * C) = (A * B) * C,mul_assocnow gives the illusion of matching, when in factMatrix.mul_associs 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_mulall the time (indeed, the lemma is now removed).