Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 00:23 9d048443

View on Github →

feat(data/int/basic): Sum of units casework lemma (#14557) This PR adds a casework lemma for when the sum of two units equals the sum of two units. I needed this lemma for irreducibility of x^n-x-1.

Estimated changes