PR !4#25481: chore: refactor Algebra.TensorProduct.rightA...

Stream: triage

[Random Issue Bot]

Today I chose PR #25481 for discussion!

chore: refactor Algebra.TensorProduct.rightAlgebra
Created by @Kevin Buzzard (@kbuzzard) on 2025-06-05
Labels: delegated, merge-conflict, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

Yes this very relevant. I'll happily fix the merge conflict once I've finished with holiday family stuff tomorrow. This was totally weird. There was discussion in Zulip and @Eric Wieser had some objections but then Damiano maintainer-merged the PR and I was really reluctant to merge it because I felt that there was still some discussion to be had (not least because I didn't understand some of the stuff people like Eric were saying) so I didn't want to merge and then the PR ended up in limbo.