Commit 2024-01-06 09:51 49f7d612

View on Github →

refactor: Split off basic Int file (#9443) Data.Int.Basic is currently made of two things:

Basic lemmas that continue the theory in Std (and could belong there, really)
Basic algebraic order instances I need the first ones earlier in the algebraic order hierarchy, hence the split. Part of #9411

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Basic.lean

deleted theorem Int.cast_eq_cast_iff_Nat

deleted theorem Int.coe_nat_div

deleted theorem Int.coe_nat_ediv

deleted theorem Int.coe_nat_inj'

deleted theorem Int.coe_nat_mod

deleted theorem Int.coe_nat_nonneg

deleted theorem Int.coe_pred_of_pos

deleted theorem Int.ediv_of_neg_of_pos

deleted theorem Int.natAbs_cast

deleted theorem Int.natAbs_ne_zero_of_ne_zero

deleted theorem Int.natAbs_surjective

deleted theorem Int.nat_succ_eq_int_succ

deleted theorem Int.neg_nat_succ

deleted theorem Int.neg_pred

deleted theorem Int.neg_succ

deleted theorem Int.ofNat_eq_cast

deleted def Int.pred

deleted theorem Int.pred_nat_succ

deleted theorem Int.pred_neg_pred

deleted theorem Int.pred_succ

deleted theorem Int.sign_coe_add_one

deleted theorem Int.sign_coe_nat_of_nonzero

deleted def Int.succ

deleted theorem Int.succ_neg_nat_succ

deleted theorem Int.succ_neg_succ

deleted theorem Int.succ_pred

deleted theorem Int.toNat_coe_nat

deleted theorem Int.toNat_coe_nat_add_one

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

deleted theorem Int.ofNat_bit0

deleted theorem Int.ofNat_bit1

Created Mathlib/Data/Int/Defs.lean

added theorem Int.cast_eq_cast_iff_Nat

added theorem Int.coe_nat_div

added theorem Int.coe_nat_ediv

added theorem Int.coe_nat_inj'

added theorem Int.coe_nat_mod

added theorem Int.coe_nat_nonneg

added theorem Int.coe_pred_of_pos

added theorem Int.ediv_of_neg_of_pos

added theorem Int.natAbs_cast

added theorem Int.natAbs_ne_zero_of_ne_zero

added theorem Int.natAbs_surjective

added theorem Int.nat_succ_eq_int_succ

added theorem Int.neg_nat_succ

added theorem Int.neg_pred

added theorem Int.neg_succ

added theorem Int.ofNat_bit0

added theorem Int.ofNat_bit1

added theorem Int.ofNat_eq_cast

added theorem Int.pow_eq

added def Int.pred

added theorem Int.pred_nat_succ

added theorem Int.pred_neg_pred

added theorem Int.pred_succ

added theorem Int.sign_coe_add_one

added theorem Int.sign_coe_nat_of_nonzero

added def Int.succ

added theorem Int.succ_neg_nat_succ

added theorem Int.succ_neg_succ

added theorem Int.succ_pred

added theorem Int.toNat_coe_nat

added theorem Int.toNat_coe_nat_add_one

Modified Mathlib/Tactic/NormNum/Pow.lean