PR #14399: feat(ring_theory/ideal/basic): define right id...

Stream: triage

[Random Issue Bot]

Today I chose PR 14399 for discussion!

feat(ring_theory/ideal/basic): define right ideals and show division rings are left and right Artinian
Created by @Oliver Nash (@ocfnash) on 2022-05-26
Labels: awaiting-author

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