Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-25 00:46 a880ea4a

View on Github →

feat(ring_theory/coprime): add some lemmas (#7650)

Estimated changes

Modified src/ring_theory/coprime.lean

added theorem is_coprime.is_unit_of_dvd'

added theorem is_coprime.neg_left

added theorem is_coprime.neg_left_iff

added theorem is_coprime.neg_neg

added theorem is_coprime.neg_neg_iff

added theorem is_coprime.neg_right

added theorem is_coprime.neg_right_iff

added theorem is_coprime.of_coprime_of_dvd_left

added theorem is_coprime.of_coprime_of_dvd_right

added theorem is_coprime.pow_iff

added theorem is_coprime.pow_left_iff

added theorem is_coprime.pow_right_iff

added theorem not_coprime_zero_zero