-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(data/matrix): little lemmas on map
#4874
Conversation
I had a couple of expressions involving `matrix.map` that the simplifier didn't `simp` away. It turns out the missing lemmas already existed, just not with the correct form / hypotheses. So here they are.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
What's the status of this PR? Was there a conclusion from the Zulip discussion linked above? |
There wasn't really a conclusion, unfortunately. A big refactor like that seems out of scope for this small PR anyway, so I'll put it on my todo list for another time and add the specialized lemmas in the suggestion for now. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@@ -353,6 +353,54 @@ lemma map_mul {L : matrix m n α} {M : matrix n o α} | |||
(L ⬝ M).map f = L.map f ⬝ M.map f := | |||
by { ext, simp [mul_apply, ring_hom.map_sum], } | |||
|
|||
/-- A version of `one_map` where `f` is a ring hom. -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Perhaps:
/-- A version of `one_map` where `f` is a ring hom. -/ | |
/-! | |
Variants of `one_map` and `zero_map` for each of the many bundled homs and equivs. | |
This hopefully won't be necessary [in future](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclasses.20for.20morphisms) | |
-/ | |
/-- A version of `one_map` where `f` is a ring hom. -/ |
or some other "this is a mess that we know about and should be discussed here" comment.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ight `simp` lemmas
I'm happy with merging this PR and creating an issue (maybe this is already done) with the ideas for the big refactor. |
Fine with this too, especially since @Vierkantor has gone to the effort of covering all the homs in this PR. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors r+
Don't forget to create the followup issue, if that's still relevant.
I had a couple of expressions involving mapping matrices, that the simplifier didn't `simp` away. It turns out the missing lemmas already existed, just not with the correct form / hypotheses. So here they are. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
map
map
This was essentially reverted in #8512 |
I had a couple of expressions involving mapping matrices, that the simplifier didn't
simp
away. It turns out the missing lemmas already existed, just not with the correct form / hypotheses. So here they are.