Commit 2022-06-02 19:38 ade30c34
View on Github →feat(data/int/basic): Lemmas for when a square equals 1 (#14501)
This PR adds two lemmas for when a square equals one. The lt lemma will be useful for irreducibility of x^n-x-1.
feat(data/int/basic): Lemmas for when a square equals 1 (#14501)
This PR adds two lemmas for when a square equals one. The lt lemma will be useful for irreducibility of x^n-x-1.