Commit 2021-12-23 14:24 c68d91da

View on Github →

feat: Init.Data.Int.{Basic, Order} (#148) Moves Data.Int.Basic to Init.Data.Int.Basic to keep the parallel with mathlib/lean3 file organization. Data.Int.Basic will be restored (with the actual contents of mathlib's data.int.basic) in a future commit.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Basic.lean

Deleted Mathlib/Data/Int/Basic.lean

deleted theorem Int.add_assoc_aux1

deleted theorem Int.add_assoc_aux2

deleted theorem Int.eq_x_or_neg

deleted theorem Int.eq_zero_ofNatAbs_eq_zero

deleted def Int.fdiv

deleted def Int.fmod

deleted def Int.gcd

deleted theorem Int.mul_negSucc_ofNat_negSucc_ofNat

deleted theorem Int.natAbs_eq

deleted theorem Int.natAbs_mul_self

deleted theorem Int.natAbs_neg

deleted theorem Int.natAbs_ofNat

deleted theorem Int.natAbs_one

deleted theorem Int.natAbs_pos_of_ne_zero

deleted theorem Int.natAbs_zero

deleted theorem Int.negOfNat_add

deleted theorem Int.negOfNat_eq_subNatNat_zero

deleted theorem Int.negOfNat_mul_negSucc_ofNat

deleted theorem Int.negOfNat_mul_ofNat

deleted theorem Int.negSucc_ofNat_add_negSucc_ofNat

deleted theorem Int.negSucc_ofNat_add_ofNat

deleted theorem Int.negSucc_ofNat_coe'

deleted theorem Int.negSucc_ofNat_coe

deleted theorem Int.negSucc_ofNat_eq

deleted theorem Int.negSucc_ofNat_inj_iff

deleted theorem Int.negSucc_ofNat_mul_negOfNat

deleted theorem Int.negSucc_ofNat_mul_subNatNat

deleted theorem Int.negSucc_ofNat_ofNat

deleted theorem Int.neg_neg_ofNat_succ

deleted theorem Int.neg_ofNat_of_succ

deleted theorem Int.neg_ofNat_zero

deleted theorem Int.ofNat_add

deleted theorem Int.ofNat_add_negSucc_ofNat

deleted theorem Int.ofNat_add_ofNat

deleted theorem Int.ofNat_eq_ofNat_iff

deleted theorem Int.ofNat_mul

deleted theorem Int.ofNat_mul_negOfNat

deleted theorem Int.ofNat_mul_negSucc_ofNat

deleted theorem Int.ofNat_mul_ofNat

deleted theorem Int.ofNat_mul_subNatNat

deleted theorem Int.ofNat_one

deleted theorem Int.ofNat_sub

deleted theorem Int.ofNat_succ

deleted theorem Int.ofNat_zero

deleted def Int.quot

deleted def Int.rem

deleted def Int.sign

deleted theorem Int.sign_mul_natAbs

deleted theorem Int.sign_neg_one

deleted theorem Int.sign_one

deleted theorem Int.sign_zero

deleted theorem Int.subNatNat_add

deleted theorem Int.subNatNat_add_add

deleted theorem Int.subNatNat_add_left

deleted theorem Int.subNatNat_add_negSucc_ofNat

deleted theorem Int.subNatNat_add_right

deleted theorem Int.subNatNat_elim

deleted theorem Int.subNatNat_of_le

deleted theorem Int.subNatNat_of_lt

deleted theorem Int.subNatNat_of_sub_eq_succ

deleted theorem Int.subNatNat_of_sub_eq_zero

deleted theorem Int.subNatNat_sub

deleted theorem Int.sub_nat_self

deleted theorem Int.toNat_sub

Modified Mathlib/Data/Nat/Basic.lean

added theorem Nat.succ_eq_one_add

Modified Mathlib/Init/Algebra/Order.lean

modified theorem le_refl

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

added theorem Int.add_assoc_aux1

added theorem Int.add_assoc_aux2

added theorem Int.eq_x_or_neg

added theorem Int.eq_zero_ofNatAbs_eq_zero

added def Int.fdiv

added def Int.fmod

added def Int.gcd

added theorem Int.mul_negSucc_ofNat_negSucc_ofNat

added theorem Int.natAbs_eq

added theorem Int.natAbs_mul_self

added theorem Int.natAbs_neg

added theorem Int.natAbs_ofNat

added theorem Int.natAbs_one

added theorem Int.natAbs_pos_of_ne_zero

added theorem Int.natAbs_zero

added theorem Int.negOfNat_add

added theorem Int.negOfNat_eq_subNatNat_zero

added theorem Int.negOfNat_mul_negSucc_ofNat

added theorem Int.negOfNat_mul_ofNat

added theorem Int.negSucc_ofNat_add_negSucc_ofNat

added theorem Int.negSucc_ofNat_add_ofNat

added theorem Int.negSucc_ofNat_coe'

added theorem Int.negSucc_ofNat_coe

added theorem Int.negSucc_ofNat_eq

added theorem Int.negSucc_ofNat_inj_iff

added theorem Int.negSucc_ofNat_mul_negOfNat

added theorem Int.negSucc_ofNat_mul_subNatNat

added theorem Int.negSucc_ofNat_ofNat

added theorem Int.neg_neg_ofNat_succ

added theorem Int.neg_ofNat_of_succ

added theorem Int.neg_ofNat_zero

added theorem Int.ofNat_add

added theorem Int.ofNat_add_negSucc_ofNat

added theorem Int.ofNat_add_ofNat

added theorem Int.ofNat_eq_ofNat_iff

added theorem Int.ofNat_mul

added theorem Int.ofNat_mul_negOfNat

added theorem Int.ofNat_mul_negSucc_ofNat

added theorem Int.ofNat_mul_ofNat

added theorem Int.ofNat_mul_subNatNat

added theorem Int.ofNat_one

added theorem Int.ofNat_sub

added theorem Int.ofNat_succ

added theorem Int.ofNat_zero

added def Int.quot

added def Int.rem

added def Int.sign

added theorem Int.sign_mul_natAbs

added theorem Int.sign_neg_one

added theorem Int.sign_one

added theorem Int.sign_zero

added theorem Int.subNatNat_add

added theorem Int.subNatNat_add_add

added theorem Int.subNatNat_add_left

added theorem Int.subNatNat_add_negSucc_ofNat

added theorem Int.subNatNat_add_right

added theorem Int.subNatNat_elim

added theorem Int.subNatNat_of_le

added theorem Int.subNatNat_of_lt

added theorem Int.subNatNat_of_sub_eq_succ

added theorem Int.subNatNat_of_sub_eq_zero

added theorem Int.subNatNat_sub

added theorem Int.sub_nat_self

added theorem Int.toNat_sub

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

added theorem Int.NonNeg.elim

added theorem Int.add_one_le_of_lt

added theorem Int.eq_natAbs_of_zero_le

added theorem Int.eq_neg_succ_of_lt_zero

added theorem Int.eq_ofNat_of_zero_le

added theorem Int.eq_one_of_mul_eq_self_left

added theorem Int.eq_one_of_mul_eq_self_right

added theorem Int.eq_succ_of_zero_lt

added theorem Int.eq_zero_of_sign_eq_zero

added theorem Int.exists_eq_neg_ofNat

added theorem Int.le.dest

added theorem Int.le.dest_sub

added theorem Int.le.intro

added theorem Int.le.intro_sub

added theorem Int.le_def

added theorem Int.le_natAbs

added theorem Int.le_of_lt

added theorem Int.le_of_lt_add_one

added theorem Int.le_of_sub_one_lt

added theorem Int.le_sub_one_of_lt

added theorem Int.lt.dest

added theorem Int.lt.intro

added theorem Int.lt_add_one_of_le

added theorem Int.lt_add_succ

added theorem Int.lt_iff_add_one_le

added theorem Int.lt_of_add_one_le

added theorem Int.lt_of_le_sub_one

added theorem Int.lt_succ

added theorem Int.mul_neg_eq_neg_mul_symm

added theorem Int.natAbs_of_nonneg

added theorem Int.neg_mul_eq_neg_mul_symm

added theorem Int.neg_of_sign_eq_neg_one

added theorem Int.neg_succ_lt_zero

added theorem Int.nonneg_def

added theorem Int.nonneg_or_nonneg_neg

added theorem Int.ofNat_le

added theorem Int.ofNat_lt

added theorem Int.ofNat_natAbs_of_nonpos

added theorem Int.ofNat_nonneg

added theorem Int.ofNat_succ_pos

added theorem Int.ofNat_zero_le

added theorem Int.pos_of_sign_eq_one

added theorem Int.sign_eq_neg_one_iff_neg

added theorem Int.sign_eq_neg_one_of_neg

added theorem Int.sign_eq_one_iff_pos

added theorem Int.sign_eq_one_of_pos

added theorem Int.sign_eq_zero_iff_zero

added theorem Int.sign_of_succ

added theorem Int.sub_one_lt_of_le

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Init/Logic.lean

added theorem Exists.imp

added def Not.elim

added theorem Not.imp

modified theorem exists_imp_exists

Modified Mathlib/Logic/Basic.lean

deleted theorem Exists.imp

deleted def Not.elim

deleted theorem Not.imp