Zulip Chat Archive

Stream: triage

Topic: issue #13506: convert `is_monoid_hom` etc to structures, ...

Random Issue Bot (Jun 04 2022 at 14:18):

Today I chose issue 13506 for discussion!

convert is_monoid_hom etc to structures, and move out of deprecated
Created by @Scott Morrison (@semorrison) on 2022-04-19
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Jul 18 2022 at 14:22):

Today I chose issue 13506 for discussion!

convert is_monoid_hom etc to structures, and move out of deprecated
Created by @Scott Morrison (@semorrison) on 2022-04-19
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Nov 30 2022 at 14:09):

Today I chose issue 13506 for discussion!

convert is_monoid_hom etc to structures, and move out of deprecated
Created by @Scott Morrison (@semorrison) on 2022-04-19
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

Random Issue Bot (Mar 11 2023 at 14:09):

Today I chose issue 13506 for discussion!

convert is_monoid_hom etc to structures, and move out of deprecated
Created by @Scott Morrison (@semorrison) on 2022-04-19
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

Last updated: Dec 20 2023 at 11:08 UTC