mul_dvd_of_coprime

Stream: Is there code for X?

[Kenny Lau]

import ring_theory.euclidean_domain

theorem mul_dvd_of_coprime {α : Type} [euclidean_domain α] (x y z : α) (H : ideal.is_coprime x y)
  (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z :=
sorry

[Kenny Lau]

Credits to @Ken Lee :

import ring_theory.euclidean_domain

theorem mul_dvd_of_coprime {α : Type} [comm_ring α] (x y z : α) (H : ideal.is_coprime x y)
  (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z :=
begin
  obtain ⟨a, b, h⟩ := ideal.is_coprime_def.1 H 1,
  rw [← mul_one z, ← h, mul_add],
  apply dvd_add,
  { rw [mul_comm z, mul_assoc],
    exact dvd_mul_of_dvd_right (mul_dvd_mul_left _ H2) _ },
  { rw [mul_comm b, ← mul_assoc],
    exact dvd_mul_of_dvd_left (mul_dvd_mul_right H1 _) _ }
end