Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 14:23 cb0a6f70

View on Github →

feat(data/int): various lemmas (#10862)

Estimated changes

Modified src/data/int/basic.lean

added theorem int.abs_sign_of_nonzero

added theorem int.is_unit_iff_abs_eq

added theorem int.of_nat_is_unit

Modified src/data/int/parity.lean

added theorem int.four_dvd_add_or_sub_of_odd

Modified src/ring_theory/int/basic.lean

added theorem int.exists_prime_and_dvd