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

Stream: triage

[Random Issue Bot]

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]

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.