Commit 2023-01-02 18:09 87a1e84c

View on Github →

feat: port data.int.lemmas (#1271)

depends on: #1159

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Lemmas.lean

added theorem Int.div2_bit

added theorem Int.injOn_natAbs_Ici

added theorem Int.injOn_natAbs_Iic

added theorem Int.le_coe_nat_sub

added theorem Int.natAbs_eq_iff_sq_eq

added theorem Int.natAbs_inj_of_nonneg_of_nonneg

added theorem Int.natAbs_inj_of_nonneg_of_nonpos

added theorem Int.natAbs_inj_of_nonpos_of_nonneg

added theorem Int.natAbs_inj_of_nonpos_of_nonpos

added theorem Int.natAbs_le_iff_sq_le

added theorem Int.natAbs_lt_iff_sq_lt

added theorem Int.strictAntiOn_natAbs

added theorem Int.strictMonoOn_natAbs

added theorem Int.succ_coe_nat_pos

added theorem Int.toNat_of_nonpos