Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+ā†‘Ctrl+ā†“to navigate, Ctrl+šŸ–±ļøto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro


! This file was ported from Lean 3 source module init.data.nat.gcd
! leanprover-community/lean commit 855e5b74e3a52a40552e8f067169d747d48743fd
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/

import Mathlib.Init.Data.Nat.Lemmas
import Mathlib.Init.Meta.WellFoundedTactics

/-!
# Definitions and properties of gcd, lcm, and coprime
-/


open WellFounded

namespace Nat

/-! gcd -/

#align nat.gcd 
Nat.gcd: ā„• ā†’ ā„• ā†’ ā„•
Nat.gcd
#align nat.gcd_zero_left 
Nat.gcd_zero_left: āˆ€ (y : ā„•), gcd 0 y = y
Nat.gcd_zero_left
#align nat.gcd_succ 
Nat.gcd_succ: āˆ€ (x y : ā„•), gcd (succ x) y = gcd (y % succ x) (succ x)
Nat.gcd_succ
#align nat.gcd_one_left 
Nat.gcd_one_left: āˆ€ (n : ā„•), gcd 1 n = 1
Nat.gcd_one_left
#align nat.gcd_self 
Nat.gcd_self: āˆ€ (n : ā„•), gcd n n = n
Nat.gcd_self
#align nat.gcd_zero_right 
Nat.gcd_zero_right: āˆ€ (n : ā„•), gcd n 0 = n
Nat.gcd_zero_right
#align nat.gcd_rec 
Nat.gcd_rec: āˆ€ (m n : ā„•), gcd m n = gcd (n % m) m
Nat.gcd_rec
#align nat.gcd.induction 
Nat.gcd.induction: āˆ€ {P : ā„• ā†’ ā„• ā†’ Prop} (m n : ā„•), (āˆ€ (n : ā„•), P 0 n) ā†’ (āˆ€ (m n : ā„•), 0 < m ā†’ P (n % m) m ā†’ P m n) ā†’ P m n
Nat.gcd.induction
#align nat.lcm 
Nat.lcm: ā„• ā†’ ā„• ā†’ ā„•
Nat.lcm

theorem 
gcd_def: āˆ€ (x y : ā„•), gcd x y = if x = 0 then y else gcd (y % x) x
gcd_def (
x: ā„•
x 
y: ā„•
y : 
ā„•: Type
ā„•) : 
gcd: ā„• ā†’ ā„• ā†’ ā„•
gcd 
x: ā„•
x 
y: ā„•
y = if 
x: ā„•
x = 
0: ?m.9
0 then 
y: ā„•
y else 
gcd: ā„• ā†’ ā„• ā†’ ā„•
gcd (
y: ā„•
y % 
x: ā„•
x) 
x: ā„•
x := 
Goals accomplished! šŸ™
x, y: ā„•

gcd x y = if x = 0 then y else gcd (y % x) x
y: ā„•

zero
gcd zero y = if zero = 0 then y else gcd (y % zero) zero
y, nāœ: ā„•

succ
gcd (succ nāœ) y = if succ nāœ = 0 then y else gcd (y % succ nāœ) (succ nāœ)
x, y: ā„•

gcd x y = if x = 0 then y else gcd (y % x) x
y: ā„•

zero
gcd zero y = if zero = 0 then y else gcd (y % zero) zero
y, nāœ: ā„•

succ
gcd (succ nāœ) y = if succ nāœ = 0 then y else gcd (y % succ nāœ) (succ nāœ)
x, y: ā„•

gcd x y = if x = 0 then y else gcd (y % x) x
Goals accomplished! šŸ™

#align nat.gcd_def 
Nat.gcd_def: āˆ€ (x y : ā„•), gcd x y = if x = 0 then y else gcd (y % x) x
Nat.gcd_def

#align nat.coprime 
Nat.coprime: ā„• ā†’ ā„• ā†’ Prop
Nat.coprime

end Nat

#align nat.gcd_dvd 
Nat.gcd_dvd: āˆ€ (m n : ā„•), Nat.gcd m n āˆ£ m āˆ§ Nat.gcd m n āˆ£ n
Nat.gcd_dvd
#align nat.gcd_dvd_left 
Nat.gcd_dvd_left: āˆ€ (m n : ā„•), Nat.gcd m n āˆ£ m
Nat.gcd_dvd_left
#align nat.gcd_dvd_right 
Nat.gcd_dvd_right: āˆ€ (m n : ā„•), Nat.gcd m n āˆ£ n
Nat.gcd_dvd_right
#align nat.gcd_le_left 
Nat.gcd_le_left: āˆ€ {m : ā„•} (n : ā„•), 0 < m ā†’ Nat.gcd m n ā‰¤ m
Nat.gcd_le_left
#align nat.gcd_le_right 
Nat.gcd_le_right: āˆ€ {m : ā„•} (n : ā„•), 0 < n ā†’ Nat.gcd m n ā‰¤ n
Nat.gcd_le_right
#align nat.dvd_gcd 
Nat.dvd_gcd: āˆ€ {k m n : ā„•}, k āˆ£ m ā†’ k āˆ£ n ā†’ k āˆ£ Nat.gcd m n
Nat.dvd_gcd
#align nat.dvd_gcd_iff 
Nat.dvd_gcd_iff: āˆ€ {k : ā„•} {m n : ā„•}, k āˆ£ Nat.gcd m n ā†” k āˆ£ m āˆ§ k āˆ£ n
Nat.dvd_gcd_iff
#align nat.gcd_comm 
Nat.gcd_comm: āˆ€ (m n : ā„•), Nat.gcd m n = Nat.gcd n m
Nat.gcd_comm
#align nat.gcd_eq_left_iff_dvd 
Nat.gcd_eq_left_iff_dvd: āˆ€ {m n : ā„•}, m āˆ£ n ā†” Nat.gcd m n = m
Nat.gcd_eq_left_iff_dvd
#align nat.gcd_eq_right_iff_dvd 
Nat.gcd_eq_right_iff_dvd: āˆ€ {m n : ā„•}, m āˆ£ n ā†” Nat.gcd n m = m
Nat.gcd_eq_right_iff_dvd
#align nat.gcd_assoc 
Nat.gcd_assoc: āˆ€ (m n k : ā„•), Nat.gcd (Nat.gcd m n) k = Nat.gcd m (Nat.gcd n k)
Nat.gcd_assoc
#align nat.gcd_one_right 
Nat.gcd_one_right: āˆ€ (n : ā„•), Nat.gcd n 1 = 1
Nat.gcd_one_right
#align nat.gcd_mul_left 
Nat.gcd_mul_left: āˆ€ (m n k : ā„•), Nat.gcd (m * n) (m * k) = m * Nat.gcd n k
Nat.gcd_mul_left
#align nat.gcd_mul_right 
Nat.gcd_mul_right: āˆ€ (m n k : ā„•), Nat.gcd (m * n) (k * n) = Nat.gcd m k * n
Nat.gcd_mul_right
#align nat.gcd_pos_of_pos_left 
Nat.gcd_pos_of_pos_left: āˆ€ {m : ā„•} (n : ā„•), 0 < m ā†’ 0 < Nat.gcd m n
Nat.gcd_pos_of_pos_left
#align nat.gcd_pos_of_pos_right 
Nat.gcd_pos_of_pos_right: āˆ€ (m : ā„•) {n : ā„•}, 0 < n ā†’ 0 < Nat.gcd m n
Nat.gcd_pos_of_pos_right
#align nat.eq_zero_of_gcd_eq_zero_left 
Nat.eq_zero_of_gcd_eq_zero_left: āˆ€ {m n : ā„•}, Nat.gcd m n = 0 ā†’ m = 0
Nat.eq_zero_of_gcd_eq_zero_left
#align nat.eq_zero_of_gcd_eq_zero_right 
Nat.eq_zero_of_gcd_eq_zero_right: āˆ€ {m n : ā„•}, Nat.gcd m n = 0 ā†’ n = 0
Nat.eq_zero_of_gcd_eq_zero_right
#align nat.gcd_div 
Nat.gcd_div: āˆ€ {m n k : ā„•}, k āˆ£ m ā†’ k āˆ£ n ā†’ Nat.gcd (m / k) (n / k) = Nat.gcd m n / k
Nat.gcd_div
#align nat.gcd_dvd_gcd_of_dvd_left 
Nat.gcd_dvd_gcd_of_dvd_left: āˆ€ {m k : ā„•} (n : ā„•), m āˆ£ k ā†’ Nat.gcd m n āˆ£ Nat.gcd k n
Nat.gcd_dvd_gcd_of_dvd_left
#align nat.gcd_dvd_gcd_of_dvd_right 
Nat.gcd_dvd_gcd_of_dvd_right: āˆ€ {m k : ā„•} (n : ā„•), m āˆ£ k ā†’ Nat.gcd n m āˆ£ Nat.gcd n k
Nat.gcd_dvd_gcd_of_dvd_right
#align nat.gcd_dvd_gcd_mul_left 
Nat.gcd_dvd_gcd_mul_left: āˆ€ (m n k : ā„•), Nat.gcd m n āˆ£ Nat.gcd (k * m) n
Nat.gcd_dvd_gcd_mul_left
#align nat.gcd_dvd_gcd_mul_right 
Nat.gcd_dvd_gcd_mul_right: āˆ€ (m n k : ā„•), Nat.gcd m n āˆ£ Nat.gcd (m * k) n
Nat.gcd_dvd_gcd_mul_right
#align nat.gcd_dvd_gcd_mul_left_right 
Nat.gcd_dvd_gcd_mul_left_right: āˆ€ (m n k : ā„•), Nat.gcd m n āˆ£ Nat.gcd m (k * n)
Nat.gcd_dvd_gcd_mul_left_right
#align nat.gcd_dvd_gcd_mul_right_right 
Nat.gcd_dvd_gcd_mul_right_right: āˆ€ (m n k : ā„•), Nat.gcd m n āˆ£ Nat.gcd m (n * k)
Nat.gcd_dvd_gcd_mul_right_right
#align nat.gcd_eq_left 
Nat.gcd_eq_left: āˆ€ {m n : ā„•}, m āˆ£ n ā†’ Nat.gcd m n = m
Nat.gcd_eq_left
#align nat.gcd_eq_right 
Nat.gcd_eq_right: āˆ€ {m n : ā„•}, n āˆ£ m ā†’ Nat.gcd m n = n
Nat.gcd_eq_right
#align nat.gcd_mul_left_left 
Nat.gcd_mul_left_left: āˆ€ (m n : ā„•), Nat.gcd (m * n) n = n
Nat.gcd_mul_left_left
#align nat.gcd_mul_left_right 
Nat.gcd_mul_left_right: āˆ€ (m n : ā„•), Nat.gcd n (m * n) = n
Nat.gcd_mul_left_right
#align nat.gcd_mul_right_left 
Nat.gcd_mul_right_left: āˆ€ (m n : ā„•), Nat.gcd (n * m) n = n
Nat.gcd_mul_right_left
#align nat.gcd_mul_right_right 
Nat.gcd_mul_right_right: āˆ€ (m n : ā„•), Nat.gcd n (n * m) = n
Nat.gcd_mul_right_right
#align nat.gcd_gcd_self_right_left 
Nat.gcd_gcd_self_right_left: āˆ€ (m n : ā„•), Nat.gcd m (Nat.gcd m n) = Nat.gcd m n
Nat.gcd_gcd_self_right_left
#align nat.gcd_gcd_self_right_right 
Nat.gcd_gcd_self_right_right: āˆ€ (m n : ā„•), Nat.gcd m (Nat.gcd n m) = Nat.gcd n m
Nat.gcd_gcd_self_right_right
#align nat.gcd_gcd_self_left_right 
Nat.gcd_gcd_self_left_right: āˆ€ (m n : ā„•), Nat.gcd (Nat.gcd n m) m = Nat.gcd n m
Nat.gcd_gcd_self_left_right
#align nat.gcd_gcd_self_left_left 
Nat.gcd_gcd_self_left_left: āˆ€ (m n : ā„•), Nat.gcd (Nat.gcd m n) m = Nat.gcd m n
Nat.gcd_gcd_self_left_left
#align nat.gcd_eq_zero_iff 
Nat.gcd_eq_zero_iff: āˆ€ {i j : ā„•}, Nat.gcd i j = 0 ā†” i = 0 āˆ§ j = 0
Nat.gcd_eq_zero_iff
#align nat.lcm_comm 
Nat.lcm_comm: āˆ€ (m n : ā„•), Nat.lcm m n = Nat.lcm n m
Nat.lcm_comm
#align nat.lcm_zero_left 
Nat.lcm_zero_left: āˆ€ (m : ā„•), Nat.lcm 0 m = 0
Nat.lcm_zero_left
#align nat.lcm_zero_right 
Nat.lcm_zero_right: āˆ€ (m : ā„•), Nat.lcm m 0 = 0
Nat.lcm_zero_right
#align nat.lcm_one_left 
Nat.lcm_one_left: āˆ€ (m : ā„•), Nat.lcm 1 m = m
Nat.lcm_one_left
#align nat.lcm_one_right 
Nat.lcm_one_right: āˆ€ (m : ā„•), Nat.lcm m 1 = m
Nat.lcm_one_right
#align nat.lcm_self 
Nat.lcm_self: āˆ€ (m : ā„•), Nat.lcm m m = m
Nat.lcm_self
#align nat.dvd_lcm_left 
Nat.dvd_lcm_left: āˆ€ (m n : ā„•), m āˆ£ Nat.lcm m n
Nat.dvd_lcm_left
#align nat.dvd_lcm_right 
Nat.dvd_lcm_right: āˆ€ (m n : ā„•), n āˆ£ Nat.lcm m n
Nat.dvd_lcm_right
#align nat.gcd_mul_lcm 
Nat.gcd_mul_lcm: āˆ€ (m n : ā„•), Nat.gcd m n * Nat.lcm m n = m * n
Nat.gcd_mul_lcm
#align nat.lcm_dvd 
Nat.lcm_dvd: āˆ€ {m n k : ā„•}, m āˆ£ k ā†’ n āˆ£ k ā†’ Nat.lcm m n āˆ£ k
Nat.lcm_dvd
#align nat.lcm_assoc 
Nat.lcm_assoc: āˆ€ (m n k : ā„•), Nat.lcm (Nat.lcm m n) k = Nat.lcm m (Nat.lcm n k)
Nat.lcm_assoc
#align nat.lcm_ne_zero 
Nat.lcm_ne_zero: āˆ€ {m n : ā„•}, m ā‰  0 ā†’ n ā‰  0 ā†’ Nat.lcm m n ā‰  0
Nat.lcm_ne_zero
#align nat.coprime_iff_gcd_eq_one 
Nat.coprime_iff_gcd_eq_one: āˆ€ {m n : ā„•}, Nat.coprime m n ā†” Nat.gcd m n = 1
Nat.coprime_iff_gcd_eq_one
#align nat.coprime.gcd_eq_one 
Nat.coprime.gcd_eq_one: āˆ€ {m n : ā„•}, Nat.coprime m n ā†’ Nat.gcd m n = 1
Nat.coprime.gcd_eq_one
#align nat.coprime.symm 
Nat.coprime.symm: āˆ€ {n m : ā„•}, Nat.coprime n m ā†’ Nat.coprime m n
Nat.coprime.symm
#align nat.coprime_comm 
Nat.coprime_comm: āˆ€ {n m : ā„•}, Nat.coprime n m ā†” Nat.coprime m n
Nat.coprime_comm
#align nat.coprime.dvd_of_dvd_mul_right 
Nat.coprime.dvd_of_dvd_mul_right: āˆ€ {k n m : ā„•}, Nat.coprime k n ā†’ k āˆ£ m * n ā†’ k āˆ£ m
Nat.coprime.dvd_of_dvd_mul_right
#align nat.coprime.dvd_of_dvd_mul_left 
Nat.coprime.dvd_of_dvd_mul_left: āˆ€ {k m n : ā„•}, Nat.coprime k m ā†’ k āˆ£ m * n ā†’ k āˆ£ n
Nat.coprime.dvd_of_dvd_mul_left
#align nat.coprime.gcd_mul_left_cancel 
Nat.coprime.gcd_mul_left_cancel: āˆ€ {k n : ā„•} (m : ā„•), Nat.coprime k n ā†’ Nat.gcd (k * m) n = Nat.gcd m n
Nat.coprime.gcd_mul_left_cancel
#align nat.coprime.gcd_mul_right_cancel 
Nat.coprime.gcd_mul_right_cancel: āˆ€ {k n : ā„•} (m : ā„•), Nat.coprime k n ā†’ Nat.gcd (m * k) n = Nat.gcd m n
Nat.coprime.gcd_mul_right_cancel
#align nat.coprime.gcd_mul_left_cancel_right 
Nat.coprime.gcd_mul_left_cancel_right: āˆ€ {k m : ā„•} (n : ā„•), Nat.coprime k m ā†’ Nat.gcd m (k * n) = Nat.gcd m n
Nat.coprime.gcd_mul_left_cancel_right
#align nat.coprime.gcd_mul_right_cancel_right 
Nat.coprime.gcd_mul_right_cancel_right: āˆ€ {k m : ā„•} (n : ā„•), Nat.coprime k m ā†’ Nat.gcd m (n * k) = Nat.gcd m n
Nat.coprime.gcd_mul_right_cancel_right
#align nat.coprime_div_gcd_div_gcd 
Nat.coprime_div_gcd_div_gcd: āˆ€ {m n : ā„•}, 0 < Nat.gcd m n ā†’ Nat.coprime (m / Nat.gcd m n) (n / Nat.gcd m n)
Nat.coprime_div_gcd_div_gcd
#align nat.not_coprime_of_dvd_of_dvd 
Nat.not_coprime_of_dvd_of_dvd: āˆ€ {d m n : ā„•}, 1 < d ā†’ d āˆ£ m ā†’ d āˆ£ n ā†’ Ā¬Nat.coprime m n
Nat.not_coprime_of_dvd_of_dvd
#align nat.exists_coprime 
Nat.exists_coprime: āˆ€ {m n : ā„•}, 0 < Nat.gcd m n ā†’ āˆƒ m' n', Nat.coprime m' n' āˆ§ m = m' * Nat.gcd m n āˆ§ n = n' * Nat.gcd m n
Nat.exists_coprime
#align nat.exists_coprime' 
Nat.exists_coprime': āˆ€ {m n : ā„•}, 0 < Nat.gcd m n ā†’ āˆƒ g m' n', 0 < g āˆ§ Nat.coprime m' n' āˆ§ m = m' * g āˆ§ n = n' * g
Nat.exists_coprime'
#align nat.coprime.mul 
Nat.coprime.mul: āˆ€ {m k n : ā„•}, Nat.coprime m k ā†’ Nat.coprime n k ā†’ Nat.coprime (m * n) k
Nat.coprime.mul
#align nat.coprime.mul_right 
Nat.coprime.mul_right: āˆ€ {k m n : ā„•}, Nat.coprime k m ā†’ Nat.coprime k n ā†’ Nat.coprime k (m * n)
Nat.coprime.mul_right
#align nat.coprime.coprime_dvd_left 
Nat.coprime.coprime_dvd_left: āˆ€ {m k n : ā„•}, m āˆ£ k ā†’ Nat.coprime k n ā†’ Nat.coprime m n
Nat.coprime.coprime_dvd_left
#align nat.coprime.coprime_dvd_right 
Nat.coprime.coprime_dvd_right: āˆ€ {n m k : ā„•}, n āˆ£ m ā†’ Nat.coprime k m ā†’ Nat.coprime k n
Nat.coprime.coprime_dvd_right
#align nat.coprime.coprime_mul_left 
Nat.coprime.coprime_mul_left: āˆ€ {k m n : ā„•}, Nat.coprime (k * m) n ā†’ Nat.coprime m n
Nat.coprime.coprime_mul_left
#align nat.coprime.coprime_mul_right 
Nat.coprime.coprime_mul_right: āˆ€ {m k n : ā„•}, Nat.coprime (m * k) n ā†’ Nat.coprime m n
Nat.coprime.coprime_mul_right
#align nat.coprime.coprime_mul_left_right 
Nat.coprime.coprime_mul_left_right: āˆ€ {m k n : ā„•}, Nat.coprime m (k * n) ā†’ Nat.coprime m n
Nat.coprime.coprime_mul_left_right
#align nat.coprime.coprime_mul_right_right 
Nat.coprime.coprime_mul_right_right: āˆ€ {m n k : ā„•}, Nat.coprime m (n * k) ā†’ Nat.coprime m n
Nat.coprime.coprime_mul_right_right
#align nat.coprime.coprime_div_left 
Nat.coprime.coprime_div_left: āˆ€ {m n a : ā„•}, Nat.coprime m n ā†’ a āˆ£ m ā†’ Nat.coprime (m / a) n
Nat.coprime.coprime_div_left
#align nat.coprime.coprime_div_right 
Nat.coprime.coprime_div_right: āˆ€ {m n a : ā„•}, Nat.coprime m n ā†’ a āˆ£ n ā†’ Nat.coprime m (n / a)
Nat.coprime.coprime_div_right
#align nat.coprime_mul_iff_left 
Nat.coprime_mul_iff_left: āˆ€ {m n k : ā„•}, Nat.coprime (m * n) k ā†” Nat.coprime m k āˆ§ Nat.coprime n k
Nat.coprime_mul_iff_left
#align nat.coprime_mul_iff_right 
Nat.coprime_mul_iff_right: āˆ€ {k m n : ā„•}, Nat.coprime k (m * n) ā†” Nat.coprime k m āˆ§ Nat.coprime k n
Nat.coprime_mul_iff_right
#align nat.coprime.gcd_left 
Nat.coprime.gcd_left: āˆ€ {m n : ā„•} (k : ā„•), Nat.coprime m n ā†’ Nat.coprime (Nat.gcd k m) n
Nat.coprime.gcd_left
#align nat.coprime.gcd_right 
Nat.coprime.gcd_right: āˆ€ {m n : ā„•} (k : ā„•), Nat.coprime m n ā†’ Nat.coprime m (Nat.gcd k n)
Nat.coprime.gcd_right
#align nat.coprime.gcd_both 
Nat.coprime.gcd_both: āˆ€ {m n : ā„•} (k l : ā„•), Nat.coprime m n ā†’ Nat.coprime (Nat.gcd k m) (Nat.gcd l n)
Nat.coprime.gcd_both
#align nat.coprime.mul_dvd_of_dvd_of_dvd 
Nat.coprime.mul_dvd_of_dvd_of_dvd: āˆ€ {m n a : ā„•}, Nat.coprime m n ā†’ m āˆ£ a ā†’ n āˆ£ a ā†’ m * n āˆ£ a
Nat.coprime.mul_dvd_of_dvd_of_dvd
#align nat.coprime_zero_left 
Nat.coprime_zero_left: āˆ€ (n : ā„•), Nat.coprime 0 n ā†” n = 1
Nat.coprime_zero_left
#align nat.coprime_zero_right 
Nat.coprime_zero_right: āˆ€ (n : ā„•), Nat.coprime n 0 ā†” n = 1
Nat.coprime_zero_right
#align nat.coprime_one_left 
Nat.coprime_one_left: āˆ€ (n : ā„•), Nat.coprime 1 n
Nat.coprime_one_left
#align nat.coprime_one_right 
Nat.coprime_one_right: āˆ€ (n : ā„•), Nat.coprime n 1
Nat.coprime_one_right
#align nat.coprime_self 
Nat.coprime_self: āˆ€ (n : ā„•), Nat.coprime n n ā†” n = 1
Nat.coprime_self
#align nat.coprime.pow_left 
Nat.coprime.pow_left: āˆ€ {m k : ā„•} (n : ā„•), Nat.coprime m k ā†’ Nat.coprime (m ^ n) k
Nat.coprime.pow_left
#align nat.coprime.pow_right 
Nat.coprime.pow_right: āˆ€ {k m : ā„•} (n : ā„•), Nat.coprime k m ā†’ Nat.coprime k (m ^ n)
Nat.coprime.pow_right
#align nat.coprime.pow 
Nat.coprime.pow: āˆ€ {k l : ā„•} (m n : ā„•), Nat.coprime k l ā†’ Nat.coprime (k ^ m) (l ^ n)
Nat.coprime.pow
#align nat.coprime.eq_one_of_dvd 
Nat.coprime.eq_one_of_dvd: āˆ€ {k m : ā„•}, Nat.coprime k m ā†’ k āˆ£ m ā†’ k = 1
Nat.coprime.eq_one_of_dvd
#align nat.gcd_mul_dvd_mul_gcd 
Nat.gcd_mul_dvd_mul_gcd: āˆ€ (k m n : ā„•), Nat.gcd k (m * n) āˆ£ Nat.gcd k m * Nat.gcd k n
Nat.gcd_mul_dvd_mul_gcd
#align nat.coprime.gcd_mul 
Nat.coprime.gcd_mul: āˆ€ {m n : ā„•} (k : ā„•), Nat.coprime m n ā†’ Nat.gcd k (m * n) = Nat.gcd k m * Nat.gcd k n
Nat.coprime.gcd_mul
#align nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul 
Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul: āˆ€ {c d a b : ā„•}, Nat.coprime c d ā†’ a * b = c * d ā†’ Nat.gcd a c * Nat.gcd b c = c
Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul