Commit 2023-08-09 22:46 cae423d8

feat: IsROrC.toStarOrderedRing as a scoped instance (#6391) With open scoped ComplexOrder, we current have StarOrderedRing Complex (as well as some other order instances). With this PR, that scope puts the same order on K where IsROrC K. There is an ongoing discussion about whether opening the scope should be required, but there is no need to address that concern simultaneously with improving behavior when the scope is already open. There also seems to be fewer downstream instance resolution issues to resolve by leaving it in the scope.