Commit 2024-05-16 08:10 2bff2343

View on Github →

chore: Move basic Int lemmas earlier (#12821) A bunch of lemmas about Int can be moved to Data.Int.Defs at little cost. This PR moves them and deletes the now empty Data.Int.Div and Data.Int.Dvd.Basic. The story is that those lemmas used to rely on lemmas proved for algebraic order structures, hence required the algebraic order instances on Int to be available. In Lean 4, those preliminary lemmas have been special-cased to Nat and Int, so there is no need for the general instances anymore (at least in basic files).

Estimated changes

Modified Archive/Imo/Imo2011Q5.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Int.lean

deleted theorem Int.cast_id

Modified Mathlib/Algebra/Order/Group/Int.lean

deleted theorem Int.add_emod_eq_add_mod_right

deleted theorem Int.ediv_dvd_ediv

deleted theorem Int.ediv_dvd_of_dvd

deleted theorem Int.le_add_one_iff

deleted theorem Int.le_sub_one_iff

deleted theorem Int.lt_of_toNat_lt

deleted theorem Int.lt_succ_self

deleted theorem Int.lt_toNat

deleted theorem Int.natAbs_eq_of_dvd_dvd

deleted theorem Int.natCast_nonpos_iff

deleted theorem Int.neg_emod_two

deleted theorem Int.pred_self_lt

deleted theorem Int.sub_one_lt_iff

deleted theorem Int.toNat_eq_zero

deleted theorem Int.toNat_le

deleted theorem Int.toNat_le_toNat

deleted theorem Int.toNat_lt_toNat

deleted theorem Int.toNat_pred_coe_of_pos

deleted theorem Int.toNat_sub_of_le

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

deleted theorem Int.emod_two_eq_zero_or_one

deleted theorem Int.exists_lt_and_lt_iff_not_dvd

deleted theorem Int.sign_add_eq_of_sign_eq

Modified Mathlib/Algebra/Ring/Int.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

deleted theorem Int.coe_nat_pow

deleted theorem Int.natCast_pos

deleted theorem Int.natCast_succ_pos

deleted theorem Int.natMod_lt

deleted theorem Int.toNat_lt'

Modified Mathlib/Data/Int/Defs.lean

added theorem Int.add_emod_eq_add_mod_right

added theorem Int.cast_id

added theorem Int.coe_nat_pow

added theorem Int.dvd_natCast

added theorem Int.dvd_of_mul_dvd_mul_left

added theorem Int.dvd_of_mul_dvd_mul_right

added theorem Int.ediv_dvd_ediv

added theorem Int.ediv_dvd_of_dvd

added theorem Int.emod_two_eq_zero_or_one

added theorem Int.eq_mul_div_of_mul_eq_mul_of_dvd_left

added theorem Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs

added theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs

added theorem Int.eq_zero_of_dvd_of_nonneg_of_lt

added theorem Int.exists_lt_and_lt_iff_not_dvd

added theorem Int.le_add_one_iff

added theorem Int.le_sub_one_iff

added theorem Int.lt_of_toNat_lt

added theorem Int.lt_succ_self

added theorem Int.lt_toNat

added theorem Int.natAbs_ediv

added theorem Int.natAbs_eq_of_dvd_dvd

added theorem Int.natAbs_le_of_dvd_ne_zero

modified theorem Int.natAbs_ofNat'

added theorem Int.natCast_dvd

added theorem Int.natCast_dvd_natCast

modified theorem Int.natCast_eq_zero

modified theorem Int.natCast_inj

added theorem Int.natCast_nonpos_iff

added theorem Int.natCast_pos

added theorem Int.natCast_succ_pos

added theorem Int.natMod_lt

added theorem Int.neg_emod_two

added theorem Int.ofNat_add_negSucc_of_ge

modified theorem Int.ofNat_eq_natCast

added theorem Int.pred_self_lt

added theorem Int.sign_add_eq_of_sign_eq

modified theorem Int.sign_natCast_of_ne_zero

added theorem Int.sub_one_lt_iff

added theorem Int.toNat_eq_zero

added theorem Int.toNat_le

added theorem Int.toNat_le_toNat

added theorem Int.toNat_lt'

added theorem Int.toNat_lt_toNat

added theorem Int.toNat_pred_coe_of_pos

added theorem Int.toNat_sub_of_le

Deleted Mathlib/Data/Int/Div.lean

deleted theorem Int.eq_mul_div_of_mul_eq_mul_of_dvd_left

deleted theorem Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs

deleted theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs

deleted theorem Int.eq_zero_of_dvd_of_nonneg_of_lt

deleted theorem Int.natAbs_le_of_dvd_ne_zero

deleted theorem Int.ofNat_add_negSucc_of_ge

Deleted Mathlib/Data/Int/Dvd/Basic.lean

deleted theorem Int.dvd_natCast

deleted theorem Int.natCast_dvd

deleted theorem Int.natCast_dvd_natCast

Modified Mathlib/Data/Int/GCD.lean

deleted theorem Int.dvd_of_mul_dvd_mul_left

deleted theorem Int.dvd_of_mul_dvd_mul_right

deleted theorem Int.natAbs_ediv

Modified Mathlib/Data/Nat/ModEq.lean

Modified Mathlib/Data/Nat/Prime.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

Modified Mathlib/Data/Rat/Lemmas.lean