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

Stream: triage

[Random Issue Bot]

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]

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