PR #3770: feat(linear_algebra): algebra multilinear maps

Stream: triage

[Random Issue Bot]

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]

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]

I'm guessing you mean #4739?

[Eric Wieser]

@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]

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]

(deleted)

[Eric Wieser]

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]

I haven't heard from Zhangir for a long time

[Eric Wieser]

I've revived the alternating map bit of that PR as #5102

[Eric Wieser]

Would appreciate if someone could take a look at my replacement PR

[Johan Commelin]

@Eric Wieser done... thanks for the ping