Skip to content
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] - refactor(Algebra/Lie/BaseChange): use new tensor product machinery #6628

Closed
wants to merge 2 commits into from

Conversation

eric-wieser
Copy link
Member


Open in Gitpod

@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR awaiting-CI labels Aug 17, 2023
@ocfnash
Copy link
Contributor

ocfnash commented Aug 17, 2023

It's great that this works but given how slow it is, it seems like we're still not ready to use TensorProduct.AlgebraTensorModule.tensorTensorTensorComm here. How about just updating the comment and leaving the implementation as it was?

@eric-wieser
Copy link
Member Author

I managed to speed it up, I didn't need the heterobasic curry after all, and that just slowed it down.
It's still a bit slower, but it's manageable.

Copy link
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, now that this is not too slow, I think it's worth doing this to have an application of TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.

It looks like further golfing is now possible (we should no longer need both bracket_tmul' and bracket_tmul and even bracket_def should not be necessary) but I don't think it's worth spending more time on this.

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Aug 17, 2023
@eric-wieser
Copy link
Member Author

Thanks, now that this is not too slow, I think it's worth doing this to have an application of TensorProduct.AlgebraTensorModule.tensorTensorTensorComm.

There's always #6306 if you want another one :)

@bors
Copy link

bors bot commented Aug 17, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title refactor(Algebra/Lie/BaseChange): use new tensor product machinery [Merged by Bors] - refactor(Algebra/Lie/BaseChange): use new tensor product machinery Aug 17, 2023
@bors bors bot closed this Aug 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants