mathlib3

71450437 - feat(algebra/group/pi): Technical casework lemma for when two binomials are equal to each other (#14400)

feat(algebra/group/pi): Technical casework lemma for when two binomials are equal to each other (#14400) This PR adds a technical casework lemma for when two binomials are equal to each other. It will be useful for irreducibility of x^n-x-1. If anyone can see how to golf the proof further, that would be appreciated!