Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-09 01:13 e14dc11a

View on Github →

feat(data/int/basic): add nat_abs_eq_nat_abs_iff_* lemmas for nonnegative and nonpositive arguments (#10611)

Estimated changes

Modified src/data/int/basic.lean

added theorem int.inj_on_nat_abs_Ici

added theorem int.inj_on_nat_abs_Iic

added theorem int.nat_abs_inj_of_nonneg_of_nonneg

added theorem int.nat_abs_inj_of_nonneg_of_nonpos

added theorem int.nat_abs_inj_of_nonpos_of_nonneg

added theorem int.nat_abs_inj_of_nonpos_of_nonpos

added theorem int.strict_anti_on_nat_abs

added theorem int.strict_mono_on_nat_abs