Commit 2022-12-01 01:59 3fc13587

View on Github →

feat: port Data.Int.Units (#807) mathlib3 SHA: 62a5626868683c104774de8d85b9855234ac807c I'm a bit confused about the choice of indenting that mathport uses in proofs - I've tried to copy it, but I can't find any documentation to explain a preferred style in Lean 4. I also added a missing #align in Algebra.Group.Units.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Units.lean

Created Mathlib/Data/Int/Units.lean

added theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one'

added theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one

added theorem Int.eq_one_or_neg_one_of_mul_eq_one'

added theorem Int.eq_one_or_neg_one_of_mul_eq_one

added theorem Int.isUnit_add_isUnit_eq_isUnit_add_isUnit

added theorem Int.isUnit_eq_one_or

added theorem Int.isUnit_eq_or_eq_neg

added theorem Int.isUnit_iff

added theorem Int.isUnit_iff_natAbs_eq

added theorem Int.isUnit_mul_self

added theorem Int.mul_eq_neg_one_iff_eq_one_or_neg_one

added theorem Int.mul_eq_one_iff_eq_one_or_neg_one

added theorem Int.ofNat_isUnit

added theorem Int.units_eq_one_or

added theorem Int.units_natAbs

Modified Mathlib/Init/Data/Int/Basic.lean