Topic: non-unital sub(semi)rings
Jireh Loreaux (Apr 20 2022 at 19:56):
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 (Apr 20 2022 at 22:12):
The deprecated stuff is hopefully all in
Yaël Dillies (Apr 20 2022 at 22:13):
And Scott is about to delete it!
Jireh Loreaux (Apr 20 2022 at 23:41):
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
Eric Wieser (Apr 21 2022 at 05:35):
I think @Anne Baanen is in the middle of such a refactor, but is away from lean at the moment
Anne Baanen (Apr 21 2022 at 08:25):
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 (Apr 21 2022 at 08:28):
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 (Apr 21 2022 at 10:22):
Glad to hear you're doing a bit better! I was indeed thinking of #11759 when I remarked it was in progress.
Jireh Loreaux (Apr 21 2022 at 12:36):
Got it, thanks! I suspected something like this must be the case.
Last updated: Aug 03 2023 at 10:10 UTC