Zulip Chat Archive
Stream: triage
Topic: issue #2534: Get rid of `is_(semi)ring_hom`
Random Issue Bot (Apr 15 2021 at 14:23):
Today I chose issue 2534 for discussion!
Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Apr 15 2021 at 14:56):
I am still confused by the goal here, and my memory is also sufficiently bad that I can never remember which is which out of is_blah_hom and is_subblah we want to keep. Both? Is the idea to delete is_subblah completely and refactor, or is the idea just to turn these things from classes to structures?
Anne Baanen (Apr 15 2021 at 15:15):
IIRC, we want to keep both is_blah_hom and is_subblah as structures.
Eric Wieser (Apr 15 2021 at 16:18):
Didn't your experiments conclude we also want a blam_hom_class?
Random Issue Bot (Jan 14 2022 at 14:18):
Today I chose issue 2534 for discussion!
Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Jan 14 2022 at 19:03):
If someone wants to make progress on this then the only undeprecated files containing deprecated imports right now are, I believe, ring_theory/free_comm_ring, group_theory/free_abelian_group and control/fold.
Random Issue Bot (Mar 18 2022 at 14:13):
Today I chose issue 2534 for discussion!
Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 15 2022 at 14:07):
Today I chose issue 2534 for discussion!
Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 29 2023 at 14:08):
Today I chose issue 2534 for discussion!
Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 28 2023 at 14:07):
Today I chose issue 2534 for discussion!
Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jul 14 2023 at 14:07):
Today I chose issue 2534 for discussion!
Get rid of is_(semi)ring_hom
Created by @Yury G. Kudryashov (@urkud) on 2020-04-25
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC