mathlib4
mathlib4 copied to clipboard
Abel tactic
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.
Wouldn't it make more sense to adapt the abel tactic from lean 3?
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.
Is this obsoleted by #555?
I think so