non-unital sub(semi)rings

Stream: general

[Jireh Loreaux]

I'm ready to define non-unital sub(semi)rings. Is there anything I should know about the current sub(semi)ring API which is outdated or deprecated? Otherwise I am planning to base my work on that.

[Kevin Buzzard]

The deprecated stuff is hopefully all in src/deprecated nowadays

[Yaël Dillies]

And Scott is about to delete it!

[Jireh Loreaux]

Sorry, I think what I mean is the parallel of the hom refactor. There the refactor is not complete and even the parts that are still have vestiges of the old format. I'm not sure if there is any similarity with the set_like stuff.

[Eric Wieser]

I think @Anne Baanen is in the middle of such a refactor, but is away from lean at the moment

[Anne Baanen]

Thanks for the ping! I was ill last week but slowly doing better. The current state is indeed that there are still some vestiges of the old approach around, especially for subobjects. But you should be able to already use the new set_like subclasses like docs#mul_mem_class and docs#add_submonoid_class.

[Anne Baanen]

Essentially, if you copy the current subsemiring definition and make sure to remove the instances that directly reference subsemiring, rather than subsemiring_class then you should be up to date with the refactor.

[Eric Wieser]

Glad to hear you're doing a bit better! I was indeed thinking of #11759 when I remarked it was in progress.

[Jireh Loreaux]

Got it, thanks! I suspected something like this must be the case.