Zulip Chat Archive

Stream: triage

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Nov 02 2020 at 02:20):

I'm guessing you mean #4739?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Nov 23 2020 at 13:37):

(deleted)

view this post on Zulip 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).

view this post on Zulip Kevin Buzzard (Nov 23 2020 at 14:25):

I haven't heard from Zhangir for a long time

view this post on Zulip Eric Wieser (Nov 24 2020 at 16:33):

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

view this post on Zulip Eric Wieser (Dec 01 2020 at 09:16):

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

view this post on Zulip Johan Commelin (Dec 01 2020 at 09:22):

@Eric Wieser done... thanks for the ping


Last updated: May 09 2021 at 16:20 UTC