Zulip Chat Archive

Stream: triage

Topic: PR #5269: feat(linear_algebra/alternating): Add dom_coprod


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
Labels: WIP

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: Dec 20 2023 at 11:08 UTC