Random Issue Bot (Dec 25 2020 at 14:27):
Today I chose PR 5269 for discussion!
feat(linear_algebra/alternating): Add dom_coprod
Created by @Eric Wieser (@eric-wieser) on 2020-12-07
Is this PR still relevant? Any recent updates? Anyone making progress?
Eric Wieser (Dec 25 2020 at 14:34):
This has some lemmas that are better handled by #5430 and don't belong in the files in this PR, but is otherwise basically ready for review
Last updated: May 09 2021 at 16:20 UTC