Commit 2023-09-05 14:01 ab52fda3

View on Github →

refactor(Data/Int/Units): golf isUnit_eq_or_eq_neg (#6952) This PR adds an IsUnit version of units_ne_iff_eq_neg and uses it to golf isUnit_eq_or_eq_neg.

Estimated changes

Modified Mathlib/Data/Int/Units.lean

modified theorem Int.isUnit_eq_or_eq_neg

added theorem Int.isUnit_ne_iff_eq_neg