Commit 2022-06-15 21:34 71450437
View on Github →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!