Commit 2024-05-15 20:27 a77c10e0

View on Github →

chore: Delete Data.Nat.Units, Data.Int.Units (#12835) The lemmas can easily move to Algebra.Group.Nat and Algebra.Group.Int, Algebra.Ring.Int respectively.

Estimated changes

added theorem Int.eq_of_mul_eq_one
added theorem Int.isUnit_eq_one_or
added theorem Int.isUnit_iff
added theorem Int.isUnit_mul_self
added theorem Int.natAbs_of_isUnit
added theorem Int.ofNat_isUnit
added theorem Int.units_natAbs
added theorem Nat.addUnits_eq_zero
added theorem Nat.units_eq_one
added theorem Int.units_eq_one_or
deleted theorem Int.eq_of_mul_eq_one
deleted theorem Int.isUnit_eq_one_or
deleted theorem Int.isUnit_eq_or_eq_neg
deleted theorem Int.isUnit_iff
deleted theorem Int.isUnit_iff_natAbs_eq
deleted theorem Int.isUnit_mul_self
deleted theorem Int.isUnit_ne_iff_eq_neg
deleted theorem Int.ofNat_isUnit
deleted theorem Int.units_eq_one_or
deleted theorem Int.units_natAbs
deleted theorem Int.units_ne_iff_eq_neg
deleted theorem Nat.addUnits_eq_zero
deleted theorem Nat.units_eq_one