Non-unital rings

Stream: maths

[Oliver Nash]

I just noticed that #11124 was merged which means we now have docs#non_unital_non_assoc_ring I was a bit surprised that it did not also include a non_unital_ring definition (for associative but not-necessarily-unital rings). Is there a reason this was left out? Could we just follow up now with a very similar PR adding non_unital_ring.

[Oliver Nash]

I expect the C* algebra people would use such class quite soon (plumbing it into docs#cstar_ring one way or another).

[Eric Wieser]

I was planning to come back and give that another review, but not a big deal. I figured it was fine to leave those out until someone cared about them, as it will just slow down typeclass search to add them. Originally we added docs#non_assoc_semiring because we thought we could use it to generalize algebra, but I never went ahead with that refactor.

[Eric Wieser]

What I was hoping to see in that PR was a generalization of some existing lemmas that now only need the new typeclass

[Oliver Nash]

I don't personally need non_unital_ring but I think it would be used. It can wait though.

[Oliver Nash]

I had imagined #11124 was the perfect roadmap so now was a good time to do it but maybe that's not quite the case.

[Oliver Nash]

I still wonder what will happen when we want the commutative version of all of these. I think we'll have to kill comm_ring and introduce is_comm.

[Kevin Buzzard]

I am not really clear on why we have both ring and comm_ring. Maybe it's just some historical accident? I think it was already there in 2017.

[Oliver Nash]

I expect so. There's the old argument about massive terms or massively-many classes.