Skip to content

Commit

Permalink
fix(data/nat/gcd): correct order of arguments in nat.coprime_mul_iff_…
Browse files Browse the repository at this point in the history
…right (#1105)

* Not sure how this works

* Fix order for coprime_mul_iff_right

* Remove spurious file
  • Loading branch information
NeilStrickland authored and mergify[bot] committed Jun 3, 2019
1 parent 38b8054 commit 4263b2b
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/data/nat/gcd.lean
Original file line number Diff line number Diff line change
Expand Up @@ -255,8 +255,8 @@ lemma coprime_mul_iff_left {k m n : ℕ} : coprime (m * n) k ↔ coprime m k ∧
⟨λ h, ⟨coprime.coprime_mul_right h, coprime.coprime_mul_left h⟩,
λ ⟨h, _⟩, by rwa [coprime, coprime.gcd_mul_left_cancel n h]⟩

lemma coprime_mul_iff_right {k m n : ℕ} : coprime k (m * n) ↔ coprime m k ∧ coprime n k :=
by rw [coprime, nat.gcd_comm]; exact coprime_mul_iff_left
lemma coprime_mul_iff_right {k m n : ℕ} : coprime k (m * n) ↔ coprime k m ∧ coprime k n :=
by { repeat { rw [coprime, nat.gcd_comm k] }, exact coprime_mul_iff_left }

lemma coprime.mul_dvd_of_dvd_of_dvd {a n m : ℕ} (hmn : coprime m n)
(hm : m ∣ a) (hn : n ∣ a) : m * n ∣ a :=
Expand Down

0 comments on commit 4263b2b

Please sign in to comment.