Zulip Chat Archive

Stream: triage

Topic: PR #5010: feat(data/fin): identities in add and mul monoids


Random Issue Bot (Jan 08 2021 at 14:32):

Today I chose PR 5010 for discussion!

feat(data/fin): identities in add and mul monoids
Created by @Yakov Pechersky (@pechersky) on 2020-11-15
Labels: WIP, awaiting-author, merge-conflict

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

Yakov Pechersky (Jan 08 2021 at 14:50):

I'd like to make this PR something about transferring the comm_ring instance or some substructure of that for fin out of data/zmod/basic to data/fin. That way there wouldn't have to be "orphan" add_comm, add_assoc and the like. I understand that one shouldn't be doing "add" or "mul" in fin, but at least given the definitions we have now, it's very hard to deal with these operations when they appear. A compromise might be to just have group and add_group and nothing more.


Last updated: Dec 20 2023 at 11:08 UTC