Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-10 15:16 12e18e8e

View on Github →

feat(data/nat/gcd): coprime add mul lemmas (#10588) Adds coprime m (n + k * m) ↔ coprime m n for nats, (and permutations thereof).

Estimated changes

Modified src/data/nat/fib.lean

Modified src/data/nat/gcd.lean

added theorem nat.coprime_add_mul_left_left

added theorem nat.coprime_add_mul_left_right

added theorem nat.coprime_add_mul_right_left

added theorem nat.coprime_add_mul_right_right

added theorem nat.coprime_mul_left_add_left

added theorem nat.coprime_mul_left_add_right

added theorem nat.coprime_mul_right_add_left

added theorem nat.coprime_mul_right_add_right

added theorem nat.gcd_add_mul_left_left

added theorem nat.gcd_add_mul_left_right

added theorem nat.gcd_add_mul_right_left

added theorem nat.gcd_add_mul_right_right

deleted theorem nat.gcd_add_mul_self

added theorem nat.gcd_mul_left_add_left

added theorem nat.gcd_mul_left_add_right

added theorem nat.gcd_mul_right_add_left

added theorem nat.gcd_mul_right_add_right