PR #2843: refactor(algebra/group/basic): minimal axioms f...

Stream: triage

[Random Issue Bot]

Today I chose PR 2843 for discussion!

refactor(algebra/group/basic): minimal axioms for group and comm_monoid
Created by @Chris Hughes (@ChrisHughes24) on 2020-05-27
Labels: WIP, merge-conflict

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

[Eric Wieser]

Should we do this, but with auto_param for the redundant lemmas instead?