Commit 2021-07-09 12:30 9a4a3ba6

View on Github →

feat(Data/Int): port data.int.basic from the lean3 prelude (#23)

port lean3 core's int/basic.lean
refactor(Int): undo my strange naming
add coe_nat_inj which I apparantly forgot about
minor cleanup
add missing imports
cleanup proofs, implementing kevin's suggestions

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

Created Mathlib/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_of_nat_abs_eq_zero

added def Int.fdiv

added def Int.fmod

added def Int.gcd

added theorem Int.mul_neg_succ_of_nat_neg_succ_of_nat

added def Int.nat_abs

added theorem Int.nat_abs_eq

added theorem Int.nat_abs_mul_self

added theorem Int.nat_abs_neg

added theorem Int.nat_abs_of_nat

added theorem Int.nat_abs_one

added theorem Int.nat_abs_pos_of_ne_zero

added theorem Int.nat_abs_zero

added def Int.nat_mod

added theorem Int.neg_neg_of_nat_succ

added def Int.neg_of_nat

added theorem Int.neg_of_nat_add

added theorem Int.neg_of_nat_eq_sub_nat_nat_zero

added theorem Int.neg_of_nat_mul_neg_succ_of_nat

added theorem Int.neg_of_nat_mul_of_nat

added theorem Int.neg_of_nat_of_succ

added theorem Int.neg_of_nat_zero

added theorem Int.neg_succ_of_nat_add_neg_succ_of_nat

added theorem Int.neg_succ_of_nat_add_of_nat

added theorem Int.neg_succ_of_nat_coe'

added theorem Int.neg_succ_of_nat_coe

added theorem Int.neg_succ_of_nat_eq

added theorem Int.neg_succ_of_nat_inj_iff

added theorem Int.neg_succ_of_nat_mul_neg_of_nat

added theorem Int.neg_succ_of_nat_mul_sub_nat_nat

added theorem Int.neg_succ_of_nat_of_nat

added def Int.nonneg

added theorem Int.of_nat_add

added theorem Int.of_nat_add_neg_succ_of_nat

added theorem Int.of_nat_add_of_nat

added theorem Int.of_nat_eq_coe

added theorem Int.of_nat_eq_of_nat_iff

added theorem Int.of_nat_mul

added theorem Int.of_nat_mul_neg_of_nat

added theorem Int.of_nat_mul_neg_succ_of_nat

added theorem Int.of_nat_mul_of_nat

added theorem Int.of_nat_mul_sub_nat_nat

added theorem Int.of_nat_one

added theorem Int.of_nat_sub

added theorem Int.of_nat_succ

added theorem Int.of_nat_zero

added def Int.quot

added def Int.rem

added def Int.sign

added theorem Int.sign_mul_nat_abs

added theorem Int.sign_neg_one

added theorem Int.sign_one

added theorem Int.sign_zero

added def Int.sub_nat_nat

added theorem Int.sub_nat_nat_add

added theorem Int.sub_nat_nat_add_add

added theorem Int.sub_nat_nat_add_left

added theorem Int.sub_nat_nat_add_neg_succ_of_nat

added theorem Int.sub_nat_nat_add_right

added theorem Int.sub_nat_nat_elim

added theorem Int.sub_nat_nat_of_le

added theorem Int.sub_nat_nat_of_lt

added theorem Int.sub_nat_nat_of_sub_eq_succ

added theorem Int.sub_nat_nat_of_sub_eq_zero

added theorem Int.sub_nat_nat_sub

added theorem Int.sub_nat_self

added def Int.to_nat

added theorem Int.to_nat_sub