Commit 2021-08-17 15:37 7bb29520

View on Github →

chore(Data.Int.Basic): naming convention, duplicate lemmasc

Estimated changes

Modified Mathlib/Data/Int/Basic.lean

modified theorem Int.eq_x_or_neg

added theorem Int.eq_zero_ofNatAbs_eq_zero

deleted theorem Int.eq_zero_of_nat_abs_eq_zero

modified def Int.gcd

added theorem Int.mul_negSucc_ofNat_negSucc_ofNat

deleted theorem Int.mul_neg_succ_of_nat_neg_succ_of_nat

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

deleted def Int.nat_abs

deleted theorem Int.nat_abs_eq

deleted theorem Int.nat_abs_mul_self

deleted theorem Int.nat_abs_neg

deleted theorem Int.nat_abs_of_nat

deleted theorem Int.nat_abs_one

deleted theorem Int.nat_abs_pos_of_ne_zero

deleted theorem Int.nat_abs_zero

deleted def Int.nat_mod

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

deleted theorem Int.neg_neg_of_nat_succ

added theorem Int.neg_ofNat_of_succ

added theorem Int.neg_ofNat_zero

deleted def Int.neg_of_nat

deleted theorem Int.neg_of_nat_add

deleted theorem Int.neg_of_nat_eq_sub_nat_nat_zero

deleted theorem Int.neg_of_nat_mul_neg_succ_of_nat

deleted theorem Int.neg_of_nat_mul_of_nat

deleted theorem Int.neg_of_nat_of_succ

deleted theorem Int.neg_of_nat_zero

deleted theorem Int.neg_succ_of_nat_add_neg_succ_of_nat

deleted theorem Int.neg_succ_of_nat_add_of_nat

deleted theorem Int.neg_succ_of_nat_coe'

deleted theorem Int.neg_succ_of_nat_coe

deleted theorem Int.neg_succ_of_nat_eq

deleted theorem Int.neg_succ_of_nat_inj_iff

deleted theorem Int.neg_succ_of_nat_mul_neg_of_nat

deleted theorem Int.neg_succ_of_nat_mul_sub_nat_nat

deleted theorem Int.neg_succ_of_nat_of_nat

deleted def Int.nonneg

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

deleted theorem Int.of_nat_add

deleted theorem Int.of_nat_add_neg_succ_of_nat

deleted theorem Int.of_nat_add_of_nat

deleted theorem Int.of_nat_eq_coe

deleted theorem Int.of_nat_eq_of_nat_iff

deleted theorem Int.of_nat_mul

deleted theorem Int.of_nat_mul_neg_of_nat

deleted theorem Int.of_nat_mul_neg_succ_of_nat

deleted theorem Int.of_nat_mul_of_nat

deleted theorem Int.of_nat_mul_sub_nat_nat

deleted theorem Int.of_nat_one

deleted theorem Int.of_nat_sub

deleted theorem Int.of_nat_succ

deleted theorem Int.of_nat_zero

added theorem Int.sign_mul_natAbs

deleted theorem Int.sign_mul_nat_abs

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

deleted def Int.sub_nat_nat

deleted theorem Int.sub_nat_nat_add

deleted theorem Int.sub_nat_nat_add_add

deleted theorem Int.sub_nat_nat_add_left

deleted theorem Int.sub_nat_nat_add_neg_succ_of_nat

deleted theorem Int.sub_nat_nat_add_right

deleted theorem Int.sub_nat_nat_elim

deleted theorem Int.sub_nat_nat_of_le

deleted theorem Int.sub_nat_nat_of_lt

deleted theorem Int.sub_nat_nat_of_sub_eq_succ

deleted theorem Int.sub_nat_nat_of_sub_eq_zero

deleted theorem Int.sub_nat_nat_sub

modified theorem Int.sub_nat_self

added theorem Int.toNat_sub

deleted def Int.to_nat

deleted theorem Int.to_nat_sub