Commit 2025-02-20 01:21 db136357

View on Github →

chore(Data/Int): split Defs into Init and Basic (#22009) This PR follows the instructions in a TODO comment in Data/Int/Defs.lean to split it into an Init.lean file for everything that doesn't meaningfully depend on Mathlib, and a Basic.lean file for things that do. I redid a few proofs in Int.Init so they are provable without reference to Mathlib.

Estimated changes

added theorem Int.dvd_natCast
added theorem Int.natAbs_surjective
added theorem Int.natCast_dvd
added theorem Int.natCast_dvd_ofNat
added theorem Int.ofNat_dvd_natCast
added theorem Int.ofNat_injective
added theorem Int.strongRec_of_ge
deleted theorem Int.dvd_natCast
deleted theorem Int.inductionOn'_add_one
deleted theorem Int.natAbs_surjective
deleted theorem Int.natCast_dvd
deleted theorem Int.natCast_dvd_natCast
deleted theorem Int.natCast_dvd_ofNat
deleted theorem Int.ofNat_dvd_natCast
deleted theorem Int.ofNat_injective
deleted theorem Int.pow_right_injective
deleted theorem Int.strongRec_of_ge