Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 15:58 d8b92599

View on Github →

feat(*): add various divisibility-related lemmas (#9866)

Estimated changes

Modified src/algebra/associated.lean

added theorem associates.mk_ne_zero

added theorem irreducible.dvd_irreducible_iff_associated

added theorem prime.dvd_prime_iff_associated

Modified src/algebra/ring/basic.lean

added theorem is_unit.neg_iff

Modified src/ring_theory/int/basic.lean

added theorem int.eq_of_associated_of_nonneg

added theorem int.nonneg_iff_normalize_eq_self

added theorem int.nonneg_of_normalize_eq_self

Modified src/ring_theory/prime.lean

added theorem prime.abs

added theorem prime.neg