Random Issue Bot (Nov 01 2020 at 22:22):
Today I chose PR 3770 for discussion!
feat(linear_algebra): algebra multilinear maps
Created by @None (@zhangir-azerbayev) on 2020-08-14
Labels: awaiting-author, merge-conflict
Is this PR still relevant? Any recent updates? Anyone making progress?
Eric Wieser (Nov 02 2020 at 01:29):
I had a go at redoing some of the permutation parts of this in #4379. @Yakov Pechersky and @Anne Baanen both had some ideas about
has_enum that would likely benefit it if they got PR'd first.
Bryan Gin-ge Chen (Nov 02 2020 at 02:20):
I'm guessing you mean #4739?
Eric Wieser (Nov 23 2020 at 10:39):
@Adam Topaz, am I right in thinking that @Zhangir Azerbayev was working with you on this? Are they likely to pick it back up, or should I try and take it over?
Adam Topaz (Nov 23 2020 at 13:27):
I wasn't really working on this PR at all... And IIRC @Zhangir Azerbayev was doing a summer project with @Kevin Buzzard . Maybe Kevin knows if Zhangir is planning to come back to this?
Eric Wieser (Nov 23 2020 at 13:37):
Eric Wieser (Nov 23 2020 at 14:24):
I've gone ahead and pushed an update to that branch that fixes the merge conflicts, and deletes all the proofs we now have elsewhere. I've tried to spin off some small PRs for uninteresting lemmas too (#5091, #5092).
Kevin Buzzard (Nov 23 2020 at 14:25):
I haven't heard from Zhangir for a long time
Eric Wieser (Nov 24 2020 at 16:33):
I've revived the alternating map bit of that PR as #5102
Eric Wieser (Dec 01 2020 at 09:16):
Would appreciate if someone could take a look at my replacement PR
Johan Commelin (Dec 01 2020 at 09:22):
@Eric Wieser done... thanks for the ping
Last updated: May 09 2021 at 16:20 UTC