Commit 2022-11-13 23:39 b7ef81c3

View on Github →

feat: align init.data.int.{basic, order} (#583)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Init/Align.lean

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

added theorem Int.eq_zero_of_natAbs_eq_zero

added theorem Int.natAbs_pos_of_ne_zero

added theorem Int.neg_negSucc

added theorem Int.ofNat_eq_coe

Deleted Mathlib/Init/Data/Int/Notation.lean

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

added theorem Int.le.elim

added theorem Int.lt.elim

added theorem Int.mul_neg_eq_neg_mul_symm

added theorem Int.neg_mul_eq_neg_mul_symm

Modified scripts/nolints.json