PR #3635: WIP: Remove the requirement from `ideal` that t...

Stream: triage

[Random Issue Bot]

Today I chose PR 3635 for discussion!

WIP: Remove the requirement from ideal that the underlying ring is commutative
Created by @Eric Wieser (@eric-wieser) on 2020-07-30
Labels: WIP, merge-conflict, please-adopt

Is this PR still relevant? Any recent updates? Anyone making progress?

[Eric Wieser]

I have little interest in continuing with this

[Mario Carneiro]

it's marked as please-adopt, that should be fine

[Bryan Gin-ge Chen]

For anyone who wants to pick this up and stumbles on this thread later, there was some discussion about non-commutative ideals in this thread.