k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
k m n : ℕ+
⊢ Coprime m k → Coprime n k → Coprime (m * n) k
repeat' rw [← coprime_coe]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime (↑m * ↑n) ↑k
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
rw [mul_coe]
no goals
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime (↑m * ↑n) ↑k
apply Nat.coprime.mul
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
rw [← coprime_coe]