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: port Algebra.Module.LinearMap #1587
Conversation
-- Porting note: adding this instance prevents a timeout in `ext_ring_op` | ||
instance {σ : R →+* S} : FunLike (M →ₛₗ[σ] M₃) M (λ _ ↦ M₃) := | ||
{ AddHomClass.toFunLike with } |
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.
This instance could be removed if we can speed up ext_ring_op
in some other way.
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.
(Indeed, with Gabriel's changes to Lean this can be deleted again.)
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.
I'm marking this as "help requested" since there are still two timeouts that I don't know how to fix.
-- *TODO*: why are you still timing out? | ||
set_option maxHeartbeats 300000 in |
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.
I don't know how to solve this timeout.
-- *TODO*: why are you still timing out? | ||
set_option maxHeartbeats 300000 in |
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.
I don't know how to solve this timeout.
leanprover/lean4#2003 solves both of the timeouts, so do we want to invest effort in fixing this ourselves? |
Co-authored-by: Johan Commelin <johan@commelin.net>
Thanks 🎉 bors merge |
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/algebra.2Emodule.2Elinear_map.20mathlib4.231587 Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: qawbecrdtey <qawbecrdtey@naver.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded:
|
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/algebra.2Emodule.2Elinear_map.20mathlib4.231587