Zulip Chat Archive

Stream: Is there code for X?

Topic: mul_dvd_of_coprime


view this post on Zulip Kenny Lau (May 23 2020 at 14:06):

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

view this post on Zulip Kenny Lau (May 23 2020 at 14:24):

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

Last updated: May 17 2021 at 15:13 UTC