mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Abel tactic

Open ChrisHughes24 opened this issue 4 years ago • 2 comments
trafficstars

I've got an Abel tactic working, but just for groups and not monoids right now. The comments are all horrible because I cut and pasted the ring tactic and adapted it to Abelian Groups.

ChrisHughes24 avatar Aug 17 '21 17:08 ChrisHughes24

Wouldn't it make more sense to adapt the abel tactic from lean 3?

digama0 avatar Aug 17 '21 18:08 digama0

I don't know. I think maybe the result would probably look pretty similar anyway, so it might not be worth it even if that is better. My plan was basically to wait until we actually have the interface for groups and monoids before finishing this off.

ChrisHughes24 avatar Aug 17 '21 18:08 ChrisHughes24

Is this obsoleted by #555?

Ruben-VandeVelde avatar Nov 15 '22 08:11 Ruben-VandeVelde

I think so

ChrisHughes24 avatar Nov 18 '22 09:11 ChrisHughes24