Commit 2021-09-29 16:59 820d0b60

View on Github →

feat: add Init/Data/Nat/Basic.lean and Init/Data/Nat/Lemmas.lean (#48) Continuing work from #34 and #35, adds Init/Data/Nat/Basic.lean and Init/Data/Nat/Lemmas.lean, corresponding to files in the Lean 3 prelude. This will help to keep a clear mapping between Lean 3 files and Lean 4 files. Populates the new files with items moved from Data/Nat/Basic.lean and Data/Nat/Gcd.lean. Fills in some missing items and leaves a few TODOs. Moves fix' in Init/Logic.lean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/Nat/Basic.lean

deleted theorem Nat.add_div_left

deleted theorem Nat.add_div_right

deleted theorem Nat.add_mod_left

deleted theorem Nat.add_mod_right

deleted theorem Nat.add_mul_div_left

deleted theorem Nat.add_mul_div_right

deleted theorem Nat.add_mul_mod_self_left

deleted theorem Nat.add_mul_mod_self_right

deleted theorem Nat.add_one_ne_zero

deleted theorem Nat.add_sub_of_le

deleted def Nat.discriminate

deleted theorem Nat.div_eq_of_lt

deleted theorem Nat.div_eq_sub_div

deleted theorem Nat.div_lt_iff_lt_mul

deleted theorem Nat.div_lt_self

deleted theorem Nat.div_mul_le_self

deleted theorem Nat.eq_of_mul_eq_mul_left

deleted theorem Nat.eq_zero_of_add_eq_zero

deleted theorem Nat.eq_zero_of_add_eq_zero_left

deleted theorem Nat.eq_zero_of_add_eq_zero_right

deleted theorem Nat.eq_zero_of_mul_eq_zero

deleted theorem Nat.eq_zero_or_eq_succ_pred

deleted theorem Nat.exists_eq_succ_of_ne_zero

deleted theorem Nat.le_div_iff_mul_le

deleted theorem Nat.le_lt_antisymm

deleted theorem Nat.le_of_le_of_sub_le_sub_right

deleted theorem Nat.le_succ_of_pred_le

deleted theorem Nat.lt_le_antisymm

deleted theorem Nat.lt_succ_of_lt

deleted theorem Nat.mod_add_div

deleted theorem Nat.mul_div_left

deleted theorem Nat.mul_div_right

deleted theorem Nat.mul_mod_left

deleted theorem Nat.mul_mod_mul_left

deleted theorem Nat.mul_mod_mul_right

deleted theorem Nat.mul_mod_right

deleted theorem Nat.mul_pred_left

deleted theorem Nat.mul_pred_right

deleted theorem Nat.mul_sub_div

deleted theorem Nat.one_add

deleted theorem Nat.one_pos

deleted theorem Nat.one_succ_zero

deleted theorem Nat.pred_inj

deleted theorem Nat.pred_lt_pred

deleted theorem Nat.pred_succ

deleted theorem Nat.pred_zero

deleted theorem Nat.sub_add_min_cancel

deleted theorem Nat.sub_eq_sub_min

deleted theorem Nat.sub_eq_zero_of_le

deleted def Nat.sub_induction

deleted theorem Nat.sub_lt_succ

deleted theorem Nat.sub_mul_div

deleted theorem Nat.sub_mul_mod

deleted theorem Nat.sub_one

deleted theorem Nat.sub_one_sub_lt

deleted theorem Nat.sub_self_add

deleted theorem Nat.succ_add_eq_succ_add

deleted theorem Nat.succ_mul_succ_eq

deleted theorem Nat.succ_ne_self

deleted theorem Nat.succ_pred_eq_of_pos

deleted theorem Nat.succ_sub

deleted theorem Nat.succ_sub_one

deleted theorem Nat.succ_sub_sub_succ

deleted def Nat.two_step_induction

Modified Mathlib/Data/Nat/Gcd.lean

deleted theorem Nat.dvd_antisymm

deleted theorem Nat.dvd_iff_mod_eq_zero

deleted theorem Nat.dvd_mod_iff

deleted theorem Nat.dvd_of_mod_eq_zero

deleted theorem Nat.dvd_sub

deleted theorem Nat.eq_one_of_dvd_one

deleted theorem Nat.le_of_dvd

deleted theorem Nat.mod_eq_zero_of_dvd

deleted theorem Nat.pos_of_dvd_of_pos

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

added theorem Nat.nat_zero_eq_zero

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

added theorem Nat.add_div_left

added theorem Nat.add_div_right

added theorem Nat.add_mod_left

added theorem Nat.add_mod_right

added theorem Nat.add_mul_div_left

added theorem Nat.add_mul_div_right

added theorem Nat.add_mul_mod_self_left

added theorem Nat.add_mul_mod_self_right

added theorem Nat.add_one_ne_zero

added def Nat.discriminate

added theorem Nat.div_eq_of_lt

added theorem Nat.div_eq_sub_div

added theorem Nat.div_lt_iff_lt_mul

added theorem Nat.div_lt_self

added theorem Nat.div_mul_le_self

added theorem Nat.dvd_antisymm

added theorem Nat.dvd_iff_mod_eq_zero

added theorem Nat.dvd_mod_iff

added theorem Nat.dvd_of_mod_eq_zero

added theorem Nat.dvd_sub

added theorem Nat.eq_one_of_dvd_one

added theorem Nat.eq_zero_of_add_eq_zero

added theorem Nat.eq_zero_of_mul_eq_zero

added theorem Nat.eq_zero_or_eq_succ_pred

added theorem Nat.exists_eq_succ_of_ne_zero

added def Nat.iterate

added theorem Nat.le_div_iff_mul_le

added theorem Nat.le_lt_antisymm

added theorem Nat.le_of_dvd

added theorem Nat.le_succ_of_pred_le

added theorem Nat.lt_le_antisymm

added theorem Nat.lt_succ_of_lt

added theorem Nat.min_succ_succ

added theorem Nat.mod_add_div

added theorem Nat.mod_eq_zero_of_dvd

added theorem Nat.mod_two_eq_zero_or_one

added theorem Nat.mul_div_left

added theorem Nat.mul_div_right

added theorem Nat.mul_mod_left

added theorem Nat.mul_mod_mul_left

added theorem Nat.mul_mod_mul_right

added theorem Nat.mul_mod_right

added theorem Nat.mul_pred_left

added theorem Nat.mul_pred_right

added theorem Nat.mul_sub_div

added theorem Nat.one_add

added theorem Nat.one_pos

added theorem Nat.one_succ_zero

added theorem Nat.pos_of_dvd_of_pos

added theorem Nat.pred_inj

added theorem Nat.pred_lt_pred

added theorem Nat.pred_succ

added theorem Nat.pred_zero

added theorem Nat.sub_eq_sub_min

added def Nat.sub_induction

added theorem Nat.sub_lt_succ

added theorem Nat.sub_mul_div

added theorem Nat.sub_mul_mod

added theorem Nat.sub_one_sub_lt

added theorem Nat.succ_add_eq_succ_add

added theorem Nat.succ_mul_succ_eq

added theorem Nat.succ_ne_self

added theorem Nat.succ_pred_eq_of_pos

added theorem Nat.succ_sub

added theorem Nat.succ_sub_one

added theorem Nat.succ_sub_sub_succ

added def Nat.two_step_induction

Modified Mathlib/Init/Logic.lean

added def WellFounded.fix'

Modified Mathlib/Logic/Basic.lean

deleted def WellFounded.fix'