Commit 2022-12-12 09:33 573c745b

View on Github →

feat: Port Data.Nat.Order.Lemmas (#927) mathlib3 SHA: 10b4e499f43088dd3bb7b5796184ad5216648ab1

Depends on #892
Depends on #907

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Positive/Ring.lean

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

added theorem Nat.Subtype.coe_bot

added theorem Nat.div_div_div_eq_div

added theorem Nat.div_eq_iff_eq_of_dvd_dvd

added theorem Nat.div_lt_div_of_lt_of_dvd

added theorem Nat.dvd_div_iff

added theorem Nat.dvd_div_of_mul_dvd

added theorem Nat.dvd_iff_div_mul_eq

added theorem Nat.dvd_iff_dvd_dvd

added theorem Nat.dvd_iff_le_div_mul

added theorem Nat.dvd_left_iff_eq

added theorem Nat.dvd_left_injective

added theorem Nat.dvd_right_iff_eq

added theorem Nat.dvd_sub'

added theorem Nat.eq_zero_of_dvd_of_lt

added theorem Nat.mod_div_self

added theorem Nat.not_dvd_iff_between_consec_multiples

added theorem Nat.set_eq_univ

added theorem Nat.succ_div

added theorem Nat.succ_div_of_dvd

added theorem Nat.succ_div_of_not_dvd

Modified Mathlib/Data/Num/Basic.lean

Modified Mathlib/Init/Algebra/Order.lean

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

Modified Mathlib/Order/Basic.lean