Commit 2022-12-17 09:19 2bbc6c2f

View on Github →

feat port: Data.Int.Order.Units (#1082) d012cd09a9b256d870751284dd6a29882b0be105

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Order/Units.lean

added theorem Int.isUnit_iff_abs_eq

added theorem Int.isUnit_sq

added theorem Int.neg_one_pow_ne_zero

added theorem Int.sq_eq_one_of_sq_le_three

added theorem Int.sq_eq_one_of_sq_lt_four

added theorem Int.units_coe_mul_self

added theorem Int.units_inv_eq_self

added theorem Int.units_mul_self

added theorem Int.units_pow_eq_pow_mod_two

added theorem Int.units_sq