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
-/
import Std.Data.Nat.Lemmas

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

-/

namespace Nat

theorem 
gcd_rec: ∀ (m n : Nat), gcd m n = gcd (n % m) m
gcd_rec
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
=
gcd: Nat → Nat → Nat
gcd
(
n: Nat
n
%
m: Nat
m
)
m: Nat
m
:= match
m: Nat
m
with |
0: Nat
0
=>

Goals accomplished! 🐙
m, n: Nat


gcd 0 n = gcd (n % 0) 0
m, n: Nat

this: n = n % 0


gcd 0 n = gcd (n % 0) 0
m, n: Nat

this: n = n % 0


gcd 0 n = gcd (n % 0) 0
m, n: Nat


gcd 0 n = gcd (n % 0) 0
m, n: Nat

this: n = n % 0


gcd 0 n = gcd (n % 0) 0
m, n: Nat

this: n = n % 0


gcd 0 n = n % 0
m, n: Nat

this: n = n % 0


gcd 0 n = n % 0
|
_: Nat
_
+ 1 =>

Goals accomplished! 🐙
m, n, n✝: Nat


gcd (n✝ + 1) n = gcd (n % (n✝ + 1)) (n✝ + 1)

Goals accomplished! 🐙
@[elab_as_elim] theorem
gcd.induction: ∀ {P : Nat → Nat → Prop} (m n : Nat), (∀ (n : Nat), P 0 n) → (∀ (m n : Nat), 0 < m → P (n % m) m → P m n) → P m n
gcd.induction
{
P: Nat → Nat → Prop
P
:
Nat: Type
Nat
→
Nat: Type
Nat
→
Prop: Type
Prop
} (
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) (
H0: ∀ (n : Nat), P 0 n
H0
: ∀
n: ?m.327
n
,
P: Nat → Nat → Prop
P
0: ?m.331
0
n: ?m.327
n
) (
H1: ∀ (m n : Nat), 0 < m → P (n % m) m → P m n
H1
: ∀
m: ?m.342
m
n: ?m.345
n
,
0: ?m.351
0
<
m: ?m.342
m
→
P: Nat → Nat → Prop
P
(
n: ?m.345
n
%
m: ?m.342
m
)
m: ?m.342
m
→
P: Nat → Nat → Prop
P
m: ?m.342
m
n: ?m.345
n
) :
P: Nat → Nat → Prop
P
m: Nat
m
n: Nat
n
:=
Nat.strongInductionOn: ∀ {motive : Nat → Sort ?u.455} (n : Nat), (∀ (n : Nat), (∀ (m : Nat), m < n → motive m) → motive n) → motive n
Nat.strongInductionOn
(motive := fun
m: ?m.457
m
=> ∀
n: ?m.460
n
,
P: Nat → Nat → Prop
P
m: ?m.457
m
n: ?m.460
n
)
m: Nat
m
(fun |
0: Nat
0
, _ =>
H0: ∀ (n : Nat), P 0 n
H0
| _+1,
IH: ∀ (m : Nat), m < n✝ + 1 → (fun m => ∀ (n : Nat), P m n) m
IH
=> fun
_: ?m.615
_
=>
H1: ∀ (m n : Nat), 0 < m → P (n % m) m → P m n
H1
_: Nat
_
_: Nat
_
(
succ_pos: ∀ (n : Nat), 0 < succ n
succ_pos
_: Nat
_
) (
IH: ∀ (m : Nat), m < n✝ + 1 → (fun m => ∀ (n : Nat), P m n) m
IH
_: Nat
_
(
mod_lt: ∀ (x : Nat) {y : Nat}, y > 0 → x % y < y
mod_lt
_: Nat
_
(
succ_pos: ∀ (n : Nat), 0 < succ n
succ_pos
_: Nat
_
))
_: Nat
_
) )
n: Nat
n
/-- The least common multiple of `m` and `n`, defined using `gcd`. -/ def
lcm: Nat → Nat → Nat
lcm
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
Nat: Type
Nat
:=
m: Nat
m
*
n: Nat
n
/
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
/-- `m` and `n` are coprime, or relatively prime, if their `gcd` is 1. -/ @[reducible] def
coprime: Nat → Nat → Prop
coprime
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
Prop: Type
Prop
:=
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
=
1: ?m.1158
1
--- theorem
gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) : (
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
m: Nat
m
) ∧ (
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
n: Nat
n
) :=

Goals accomplished! 🐙
m, n: Nat


gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat


gcd m n ∣ m ∧ gcd m n ∣ n
n: Nat


H0
gcd 0 n ∣ 0 ∧ gcd 0 n ∣ n
n: Nat


H0
gcd 0 n ∣ 0 ∧ gcd 0 n ∣ n
n: Nat


H0
n: Nat


H0
n: Nat


H0
n: Nat


H0
gcd 0 n ∣ 0 ∧ gcd 0 n ∣ n

Goals accomplished! 🐙
m, n: Nat


gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat

a✝: 0 < m

IH: gcd (n % m) m ∣ n % m ∧ gcd (n % m) m ∣ m


H1
gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat

a✝: 0 < m

IH: gcd (n % m) m ∣ n % m ∧ gcd (n % m) m ∣ m


H1
gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m


H1
gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m


H1
gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m


H1
gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat

a✝: 0 < m

IH: gcd m n ∣ n % m ∧ gcd m n ∣ m


H1
gcd m n ∣ m ∧ gcd m n ∣ n
m, n: Nat

a✝: 0 < m

IH: gcd (n % m) m ∣ n % m ∧ gcd (n % m) m ∣ m


H1
gcd m n ∣ m ∧ gcd m n ∣ n

Goals accomplished! 🐙
theorem
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
m: Nat
m
:= (
gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd
m: Nat
m
n: Nat
n
).
left: ∀ {a b : Prop}, a ∧ b → a
left
theorem
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
n: Nat
n
:= (
gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd
m: Nat
m
n: Nat
n
).
right: ∀ {a b : Prop}, a ∧ b → b
right
theorem
gcd_le_left: ∀ {m : Nat} (n : Nat), 0 < m → gcd m n ≤ m
gcd_le_left
(
n: ?m.1383
n
) (
h: 0 < m
h
:
0: ?m.1388
0
<
m: ?m.1380
m
) :
gcd: Nat → Nat → Nat
gcd
m: ?m.1380
m
n: ?m.1383
n
≤
m: ?m.1380
m
:=
le_of_dvd: ∀ {m n : Nat}, 0 < n → m ∣ n → m ≤ n
le_of_dvd
h: 0 < m
h
<|
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
m: Nat
m
n: Nat
n
theorem
gcd_le_right: ∀ {m : Nat} (n : Nat), 0 < n → gcd m n ≤ n
gcd_le_right
(
n: ?m.1513
n
) (
h: 0 < n
h
:
0: ?m.1518
0
<
n: ?m.1513
n
) :
gcd: Nat → Nat → Nat
gcd
m: ?m.1510
m
n: ?m.1513
n
≤
n: ?m.1513
n
:=
le_of_dvd: ∀ {m n : Nat}, 0 < n → m ∣ n → m ≤ n
le_of_dvd
h: 0 < n
h
<|
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
n: Nat
n
theorem
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
:
k: ?m.1599
k
∣
m: ?m.1609
m
→
k: ?m.1599
k
∣
n: ?m.1629
n
→
k: ?m.1599
k
∣
gcd: Nat → Nat → Nat
gcd
m: ?m.1609
m
n: ?m.1629
n
:=

Goals accomplished! 🐙
k, m, n: Nat


k ∣ m → k ∣ n → k ∣ gcd m n
k, m, n: Nat


k ∣ m → k ∣ n → k ∣ gcd m n
k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m


H1
k ∣ gcd n m
k, m, n: Nat


k ∣ m → k ∣ n → k ∣ gcd m n
k, n: Nat

km: k ∣ 0

kn: k ∣ n


H0
k ∣ gcd 0 n
k, n: Nat

km: k ∣ 0

kn: k ∣ n


H0
k ∣ gcd 0 n
k, n: Nat

km: k ∣ 0

kn: k ∣ n


H0
k ∣ n
k, n: Nat

km: k ∣ 0

kn: k ∣ n


H0
k ∣ n
k, n: Nat

km: k ∣ 0

kn: k ∣ n


H0
k ∣ n
k, n: Nat

km: k ∣ 0

kn: k ∣ n


H0
k ∣ gcd 0 n

Goals accomplished! 🐙
k, m, n: Nat


k ∣ m → k ∣ n → k ∣ gcd m n
k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m


H1
k ∣ gcd n m
k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m


H1
k ∣ gcd n m
k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m


H1
k ∣ gcd (m % n) n
k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m


H1
k ∣ gcd (m % n) n
k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m


H1
k ∣ gcd (m % n) n
k, n, m: Nat

a✝: 0 < n

IH: k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n

km: k ∣ n

kn: k ∣ m


H1
k ∣ gcd n m

Goals accomplished! 🐙
theorem
dvd_gcd_iff: ∀ {k : Nat} {m n : Nat}, k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n
dvd_gcd_iff
:
k: ?m.1788
k
∣
gcd: Nat → Nat → Nat
gcd
m: ?m.1795
m
n: ?m.1802
n
↔
k: ?m.1788
k
∣
m: ?m.1795
m
∧
k: ?m.1788
k
∣
n: ?m.1802
n
:= ⟨fun
h: ?m.1829
h
=> let ⟨
h₁: gcd m n ∣ m
h₁
,
h₂: gcd m n ∣ n
h₂
⟩ :=
gcd_dvd: ∀ (m n : Nat), gcd m n ∣ m ∧ gcd m n ∣ n
gcd_dvd
m: Nat
m
n: Nat
n
; ⟨
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
h: ?m.1829
h
h₁: gcd m n ∣ m
h₁
,
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
h: ?m.1829
h
h₂: gcd m n ∣ n
h₂
⟩, fun ⟨
h₁: k ∣ m
h₁
,
h₂: k ∣ n
h₂
⟩ =>
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
h₁: k ∣ m
h₁
h₂: k ∣ n
h₂
⟩ theorem
gcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
=
gcd: Nat → Nat → Nat
gcd
n: Nat
n
m: Nat
m
:=
dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
(
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
n: Nat
n
) (
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
m: Nat
m
n: Nat
n
)) (
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
n: Nat
n
m: Nat
m
) (
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
n: Nat
n
m: Nat
m
)) theorem
gcd_eq_left_iff_dvd: ∀ {m n : Nat}, m ∣ n ↔ gcd m n = m
gcd_eq_left_iff_dvd
:
m: ?m.2071
m
∣
n: ?m.2078
n
↔
gcd: Nat → Nat → Nat
gcd
m: ?m.2071
m
n: ?m.2078
n
=
m: ?m.2071
m
:= ⟨fun
h: ?m.2105
h
=>

Goals accomplished! 🐙
m, n: Nat

h: m ∣ n


gcd m n = m
m, n: Nat

h: m ∣ n


gcd m n = m
m, n: Nat

h: m ∣ n


gcd (n % m) m = m
m, n: Nat

h: m ∣ n


gcd m n = m
m, n: Nat

h: m ∣ n


gcd 0 m = m
m, n: Nat

h: m ∣ n


gcd m n = m
m, n: Nat

h: m ∣ n


m = m

Goals accomplished! 🐙
, fun
h: ?m.2112
h
=>
h: ?m.2112
h
▸
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
n: Nat
n
⟩ theorem
gcd_eq_right_iff_dvd: ∀ {m n : Nat}, m ∣ n ↔ gcd n m = m
gcd_eq_right_iff_dvd
:
m: ?m.2165
m
∣
n: ?m.2172
n
↔
gcd: Nat → Nat → Nat
gcd
n: ?m.2172
n
m: ?m.2165
m
=
m: ?m.2165
m
:=

Goals accomplished! 🐙
m, n: Nat


m ∣ n ↔ gcd n m = m
m, n: Nat


m ∣ n ↔ gcd n m = m
m, n: Nat


m ∣ n ↔ gcd m n = m
m, n: Nat


m ∣ n ↔ gcd m n = m
m, n: Nat


m ∣ n ↔ gcd m n = m
m, n: Nat


m ∣ n ↔ gcd n m = m

Goals accomplished! 🐙
theorem
gcd_assoc: ∀ (m n k : Nat), gcd (gcd m n) k = gcd m (gcd n k)
gcd_assoc
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
(
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
)
k: Nat
k
=
gcd: Nat → Nat → Nat
gcd
m: Nat
m
(
gcd: Nat → Nat → Nat
gcd
n: Nat
n
k: Nat
k
) :=
dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
(
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
(
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
)
k: Nat
k
) (
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
m: Nat
m
n: Nat
n
)) (
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
(
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
)
k: Nat
k
) (
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
n: Nat
n
)) (
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
(
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
)
k: Nat
k
))) (
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
m: Nat
m
(
gcd: Nat → Nat → Nat
gcd
n: Nat
n
k: Nat
k
)) (
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
(
gcd: Nat → Nat → Nat
gcd
n: Nat
n
k: Nat
k
)) (
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
n: Nat
n
k: Nat
k
))) (
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
(
gcd: Nat → Nat → Nat
gcd
n: Nat
n
k: Nat
k
)) (
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
n: Nat
n
k: Nat
k
))) @[simp] theorem
gcd_one_right: ∀ (n : Nat), gcd n 1 = 1
gcd_one_right
(
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
n: Nat
n
1: ?m.2280
1
=
1: ?m.2289
1
:= (
gcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm
n: Nat
n
1: ?m.2306
1
).
trans: ∀ {α : Sort ?u.2308} {a b c : α}, a = b → b = c → a = c
trans
(
gcd_one_left: ∀ (n : Nat), gcd 1 n = 1
gcd_one_left
n: Nat
n
) theorem
gcd_mul_left: ∀ (m n k : Nat), gcd (m * n) (m * k) = m * gcd n k
gcd_mul_left
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
(
m: Nat
m
*
n: Nat
n
) (
m: Nat
m
*
k: Nat
k
) =
m: Nat
m
*
gcd: Nat → Nat → Nat
gcd
n: Nat
n
k: Nat
k
:=

Goals accomplished! 🐙
m, n, k: Nat


gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat


gcd (m * n) (m * k) = m * gcd n k
m, k: Nat


H0
gcd (m * 0) (m * k) = m * gcd 0 k

Goals accomplished! 🐙
m, n, k: Nat


gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n


H1
gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n


H1
gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * k % (m * n)) (m * n) = m * gcd (k % n) n


H1
gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n


H1
gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * n) (m * k) = m * gcd (k % n) n


H1
gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * (k % n)) (m * n) = m * gcd (k % n) n


H1
gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * n) (m * k) = m * gcd n k


H1
gcd (m * n) (m * k) = m * gcd n k
m, n, k: Nat

a✝: 0 < n

IH: gcd (m * n) (m * k) = m * gcd n k


H1
gcd (m * n) (m * k) = m * gcd n k

Goals accomplished! 🐙
theorem
gcd_mul_right: ∀ (m n k : Nat), gcd (m * n) (k * n) = gcd m k * n
gcd_mul_right
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
(
m: Nat
m
*
n: Nat
n
) (
k: Nat
k
*
n: Nat
n
) =
gcd: Nat → Nat → Nat
gcd
m: Nat
m
k: Nat
k
*
n: Nat
n
:=

Goals accomplished! 🐙
m, n, k: Nat


gcd (m * n) (k * n) = gcd m k * n
m, n, k: Nat


gcd (m * n) (k * n) = gcd m k * n
m, n, k: Nat


gcd (n * m) (k * n) = gcd m k * n
m, n, k: Nat


gcd (m * n) (k * n) = gcd m k * n
m, n, k: Nat


gcd (n * m) (n * k) = gcd m k * n
m, n, k: Nat


gcd (m * n) (k * n) = gcd m k * n
m, n, k: Nat


gcd (n * m) (n * k) = n * gcd m k
m, n, k: Nat


gcd (m * n) (k * n) = gcd m k * n
m, n, k: Nat


n * gcd m k = n * gcd m k

Goals accomplished! 🐙
theorem
gcd_pos_of_pos_left: ∀ {m : Nat} (n : Nat), 0 < m → 0 < gcd m n
gcd_pos_of_pos_left
{
m: Nat
m
:
Nat: Type
Nat
} (
n: Nat
n
:
Nat: Type
Nat
) (
mpos: 0 < m
mpos
:
0: ?m.2747
0
<
m: Nat
m
) :
0: ?m.2775
0
<
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
:=
pos_of_dvd_of_pos: ∀ {m n : Nat}, m ∣ n → 0 < n → 0 < m
pos_of_dvd_of_pos
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
m: Nat
m
n: Nat
n
)
mpos: 0 < m
mpos
theorem
gcd_pos_of_pos_right: ∀ (m : Nat) {n : Nat}, 0 < n → 0 < gcd m n
gcd_pos_of_pos_right
(
m: Nat
m
:
Nat: Type
Nat
) {
n: Nat
n
:
Nat: Type
Nat
} (
npos: 0 < n
npos
:
0: ?m.2818
0
<
n: Nat
n
) :
0: ?m.2846
0
<
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
:=
pos_of_dvd_of_pos: ∀ {m n : Nat}, m ∣ n → 0 < n → 0 < m
pos_of_dvd_of_pos
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
n: Nat
n
)
npos: 0 < n
npos
theorem
div_gcd_pos_of_pos_left: ∀ {a : Nat} (b : Nat), 0 < a → 0 < a / gcd a b
div_gcd_pos_of_pos_left
(
b: Nat
b
:
Nat: Type
Nat
) (
h: 0 < a
h
:
0: ?m.2906
0
<
a: ?m.2899
a
) :
0: ?m.2949
0
<
a: ?m.2899
a
/
a: ?m.2899
a
.
gcd: Nat → Nat → Nat
gcd
b: Nat
b
:= (
Nat.le_div_iff_mul_le: ∀ {k x y : Nat}, 0 < k → (x ≤ y / k ↔ x * k ≤ y)
Nat.le_div_iff_mul_le
<|
Nat.gcd_pos_of_pos_left: ∀ {m : Nat} (n : Nat), 0 < m → 0 < gcd m n
Nat.gcd_pos_of_pos_left
_: Nat
_
h: 0 < a
h
).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
(
Nat.one_mul: ∀ (n : Nat), 1 * n = n
Nat.one_mul
_: Nat
_
▸
Nat.gcd_le_left: ∀ {m : Nat} (n : Nat), 0 < m → gcd m n ≤ m
Nat.gcd_le_left
_: Nat
_
h: 0 < a
h
) theorem
div_gcd_pos_of_pos_right: ∀ {b : Nat} (a : Nat), 0 < b → 0 < b / gcd a b
div_gcd_pos_of_pos_right
(
a: Nat
a
:
Nat: Type
Nat
) (
h: 0 < b
h
:
0: ?m.3173
0
<
b: ?m.3166
b
) :
0: ?m.3216
0
<
b: ?m.3166
b
/
a: Nat
a
.
gcd: Nat → Nat → Nat
gcd
b: ?m.3166
b
:= (
Nat.le_div_iff_mul_le: ∀ {k x y : Nat}, 0 < k → (x ≤ y / k ↔ x * k ≤ y)
Nat.le_div_iff_mul_le
<|
Nat.gcd_pos_of_pos_right: ∀ (m : Nat) {n : Nat}, 0 < n → 0 < gcd m n
Nat.gcd_pos_of_pos_right
_: Nat
_
h: 0 < b
h
).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
(
Nat.one_mul: ∀ (n : Nat), 1 * n = n
Nat.one_mul
_: Nat
_
▸
Nat.gcd_le_right: ∀ {m : Nat} (n : Nat), 0 < n → gcd m n ≤ n
Nat.gcd_le_right
_: Nat
_
h: 0 < b
h
) theorem
eq_zero_of_gcd_eq_zero_left: ∀ {m n : Nat}, gcd m n = 0 → m = 0
eq_zero_of_gcd_eq_zero_left
{
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
} (
H: gcd m n = 0
H
:
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
=
0: ?m.3345
0
) :
m: Nat
m
=
0: ?m.3367
0
:= match
eq_zero_or_pos: ∀ (n : Nat), n = 0 ∨ n > 0
eq_zero_or_pos
m: Nat
m
with |
.inl: ∀ {a b : Prop}, a → a ∨ b
.inl
H0: m = 0
H0
=>
H0: m = 0
H0
|
.inr: ∀ {a b : Prop}, b → a ∨ b
.inr
H1: m > 0
H1
=>
absurd: ∀ {a : Prop} {b : Sort ?u.3408}, a → ¬a → b
absurd
(
Eq.symm: ∀ {α : Sort ?u.3411} {a b : α}, a = b → b = a
Eq.symm
H: gcd m n = 0
H
) (
ne_of_lt: ∀ {a b : Nat}, a < b → a ≠ b
ne_of_lt
(
gcd_pos_of_pos_left: ∀ {m : Nat} (n : Nat), 0 < m → 0 < gcd m n
gcd_pos_of_pos_left
_: Nat
_
H1: m > 0
H1
)) theorem
eq_zero_of_gcd_eq_zero_right: ∀ {m n : Nat}, gcd m n = 0 → n = 0
eq_zero_of_gcd_eq_zero_right
{
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
} (
H: gcd m n = 0
H
:
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
=
0: ?m.3511
0
) :
n: Nat
n
=
0: ?m.3533
0
:=

Goals accomplished! 🐙
m, n: Nat

H: gcd m n = 0


n = 0
m, n: Nat

H: gcd m n = 0


n = 0
m, n: Nat

H: gcd n m = 0


n = 0
m, n: Nat

H: gcd n m = 0


n = 0
m, n: Nat

H: gcd n m = 0


n = 0
m, n: Nat

H: gcd m n = 0


n = 0

Goals accomplished! 🐙
theorem
gcd_ne_zero_left: ∀ {m n : Nat}, m ≠ 0 → gcd m n ≠ 0
gcd_ne_zero_left
:
m: ?m.3590
m
≠
0: ?m.3617
0
→
gcd: Nat → Nat → Nat
gcd
m: ?m.3590
m
n: ?m.3610
n
≠
0: ?m.3630
0
:=
mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt
eq_zero_of_gcd_eq_zero_left: ∀ {m n : Nat}, gcd m n = 0 → m = 0
eq_zero_of_gcd_eq_zero_left
theorem
gcd_ne_zero_right: ∀ {n m : Nat}, n ≠ 0 → gcd m n ≠ 0
gcd_ne_zero_right
:
n: ?m.3673
n
≠
0: ?m.3700
0
→
gcd: Nat → Nat → Nat
gcd
m: ?m.3693
m
n: ?m.3673
n
≠
0: ?m.3713
0
:=
mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt
eq_zero_of_gcd_eq_zero_right: ∀ {m n : Nat}, gcd m n = 0 → n = 0
eq_zero_of_gcd_eq_zero_right
theorem
gcd_div: ∀ {m n k : Nat}, k ∣ m → k ∣ n → gcd (m / k) (n / k) = gcd m n / k
gcd_div
{
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
} (
H1: k ∣ m
H1
:
k: Nat
k
∣
m: Nat
m
) (
H2: k ∣ n
H2
:
k: Nat
k
∣
n: Nat
n
) :
gcd: Nat → Nat → Nat
gcd
(
m: Nat
m
/
k: Nat
k
) (
n: Nat
n
/
k: Nat
k
) =
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
/
k: Nat
k
:= match
eq_zero_or_pos: ∀ (n : Nat), n = 0 ∨ n > 0
eq_zero_or_pos
k: Nat
k
with |
.inl: ∀ {a b : Prop}, a → a ∨ b
.inl
H0: k = 0
H0
=>

Goals accomplished! 🐙
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H0: k = 0


gcd (m / k) (n / k) = gcd m n / k

Goals accomplished! 🐙
|
.inr: ∀ {a b : Prop}, b → a ∨ b
.inr
H3: k > 0
H3
=>

Goals accomplished! 🐙
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) = gcd m n / k
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) * k = gcd m n / k * k
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) = gcd m n / k
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) * k = gcd m n / k * k
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) * k = gcd m n
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) * k = gcd m n / k * k
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k * k) (n / k * k) = gcd m n
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) * k = gcd m n / k * k
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd m (n / k * k) = gcd m n
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd (m / k) (n / k) * k = gcd m n / k * k
m, n, k: Nat

H1: k ∣ m

H2: k ∣ n

H3: k > 0


gcd m n = gcd m n

Goals accomplished! 🐙
theorem
gcd_dvd_gcd_of_dvd_left: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd m n ∣ gcd k n
gcd_dvd_gcd_of_dvd_left
{
m: Nat
m
k: Nat
k
:
Nat: Type
Nat
} (
n: Nat
n
:
Nat: Type
Nat
) (
H: m ∣ k
H
:
m: Nat
m
∣
k: Nat
k
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
gcd: Nat → Nat → Nat
gcd
k: Nat
k
n: Nat
n
:=
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
m: Nat
m
n: Nat
n
)
H: m ∣ k
H
) (
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
m: Nat
m
n: Nat
n
) theorem
gcd_dvd_gcd_of_dvd_right: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd n m ∣ gcd n k
gcd_dvd_gcd_of_dvd_right
{
m: Nat
m
k: Nat
k
:
Nat: Type
Nat
} (
n: Nat
n
:
Nat: Type
Nat
) (
H: m ∣ k
H
:
m: Nat
m
∣
k: Nat
k
) :
gcd: Nat → Nat → Nat
gcd
n: Nat
n
m: Nat
m
∣
gcd: Nat → Nat → Nat
gcd
n: Nat
n
k: Nat
k
:=
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
n: Nat
n
m: Nat
m
) (
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
n: Nat
n
m: Nat
m
)
H: m ∣ k
H
) theorem
gcd_dvd_gcd_mul_left: ∀ (m n k : Nat), gcd m n ∣ gcd (k * m) n
gcd_dvd_gcd_mul_left
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
gcd: Nat → Nat → Nat
gcd
(
k: Nat
k
*
m: Nat
m
)
n: Nat
n
:=
gcd_dvd_gcd_of_dvd_left: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd m n ∣ gcd k n
gcd_dvd_gcd_of_dvd_left
_: Nat
_
(
Nat.dvd_mul_left: ∀ (a b : Nat), a ∣ b * a
Nat.dvd_mul_left
_: Nat
_
_: Nat
_
) theorem
gcd_dvd_gcd_mul_right: ∀ (m n k : Nat), gcd m n ∣ gcd (m * k) n
gcd_dvd_gcd_mul_right
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
gcd: Nat → Nat → Nat
gcd
(
m: Nat
m
*
k: Nat
k
)
n: Nat
n
:=
gcd_dvd_gcd_of_dvd_left: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd m n ∣ gcd k n
gcd_dvd_gcd_of_dvd_left
_: Nat
_
(
Nat.dvd_mul_right: ∀ (a b : Nat), a ∣ a * b
Nat.dvd_mul_right
_: Nat
_
_: Nat
_
) theorem
gcd_dvd_gcd_mul_left_right: ∀ (m n k : Nat), gcd m n ∣ gcd m (k * n)
gcd_dvd_gcd_mul_left_right
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
gcd: Nat → Nat → Nat
gcd
m: Nat
m
(
k: Nat
k
*
n: Nat
n
) :=
gcd_dvd_gcd_of_dvd_right: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd n m ∣ gcd n k
gcd_dvd_gcd_of_dvd_right
_: Nat
_
(
Nat.dvd_mul_left: ∀ (a b : Nat), a ∣ b * a
Nat.dvd_mul_left
_: Nat
_
_: Nat
_
) theorem
gcd_dvd_gcd_mul_right_right: ∀ (m n k : Nat), gcd m n ∣ gcd m (n * k)
gcd_dvd_gcd_mul_right_right
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
∣
gcd: Nat → Nat → Nat
gcd
m: Nat
m
(
n: Nat
n
*
k: Nat
k
) :=
gcd_dvd_gcd_of_dvd_right: ∀ {m k : Nat} (n : Nat), m ∣ k → gcd n m ∣ gcd n k
gcd_dvd_gcd_of_dvd_right
_: Nat
_
(
Nat.dvd_mul_right: ∀ (a b : Nat), a ∣ a * b
Nat.dvd_mul_right
_: Nat
_
_: Nat
_
) theorem
gcd_eq_left: ∀ {m n : Nat}, m ∣ n → gcd m n = m
gcd_eq_left
{
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
} (
H: m ∣ n
H
:
m: Nat
m
∣
n: Nat
n
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
=
m: Nat
m
:=
dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
_: Nat
_
_: Nat
_
) (
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
Nat.dvd_refl: ∀ (a : Nat), a ∣ a
Nat.dvd_refl
_: Nat
_
)
H: m ∣ n
H
) theorem
gcd_eq_right: ∀ {m n : Nat}, n ∣ m → gcd m n = n
gcd_eq_right
{
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
} (
H: n ∣ m
H
:
n: Nat
n
∣
m: Nat
m
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
=
n: Nat
n
:=

Goals accomplished! 🐙
m, n: Nat

H: n ∣ m


gcd m n = n
m, n: Nat

H: n ∣ m


gcd m n = n
m, n: Nat

H: n ∣ m


gcd n m = n
m, n: Nat

H: n ∣ m


gcd m n = n
m, n: Nat

H: n ∣ m


n = n

Goals accomplished! 🐙
@[simp] theorem
gcd_mul_left_left: ∀ (m n : Nat), gcd (m * n) n = n
gcd_mul_left_left
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
(
m: Nat
m
*
n: Nat
n
)
n: Nat
n
=
n: Nat
n
:=
dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
_: Nat
_
_: Nat
_
) (
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
Nat.dvd_mul_left: ∀ (a b : Nat), a ∣ b * a
Nat.dvd_mul_left
_: Nat
_
_: Nat
_
) (
Nat.dvd_refl: ∀ (a : Nat), a ∣ a
Nat.dvd_refl
_: Nat
_
)) @[simp] theorem
gcd_mul_left_right: ∀ (m n : Nat), gcd n (m * n) = n
gcd_mul_left_right
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
n: Nat
n
(
m: Nat
m
*
n: Nat
n
) =
n: Nat
n
:=

Goals accomplished! 🐙
m, n: Nat


gcd n (m * n) = n
m, n: Nat


gcd n (m * n) = n
m, n: Nat


gcd (m * n) n = n
m, n: Nat


gcd n (m * n) = n
m, n: Nat


n = n

Goals accomplished! 🐙
@[simp] theorem
gcd_mul_right_left: ∀ (m n : Nat), gcd (n * m) n = n
gcd_mul_right_left
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
(
n: Nat
n
*
m: Nat
m
)
n: Nat
n
=
n: Nat
n
:=

Goals accomplished! 🐙
m, n: Nat


gcd (n * m) n = n
m, n: Nat


gcd (n * m) n = n
m, n: Nat


gcd (m * n) n = n
m, n: Nat


gcd (n * m) n = n
m, n: Nat


n = n

Goals accomplished! 🐙
@[simp] theorem
gcd_mul_right_right: ∀ (m n : Nat), gcd n (n * m) = n
gcd_mul_right_right
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
n: Nat
n
(
n: Nat
n
*
m: Nat
m
) =
n: Nat
n
:=

Goals accomplished! 🐙
m, n: Nat


gcd n (n * m) = n
m, n: Nat


gcd n (n * m) = n
m, n: Nat


gcd (n * m) n = n
m, n: Nat


gcd n (n * m) = n
m, n: Nat


n = n

Goals accomplished! 🐙
@[simp] theorem
gcd_gcd_self_right_left: ∀ (m n : Nat), gcd m (gcd m n) = gcd m n
gcd_gcd_self_right_left
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
(
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
) =
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
:=
dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
(
gcd_dvd_right: ∀ (m n : Nat), gcd m n ∣ n
gcd_dvd_right
_: Nat
_
_: Nat
_
) (
dvd_gcd: ∀ {k m n : Nat}, k ∣ m → k ∣ n → k ∣ gcd m n
dvd_gcd
(
gcd_dvd_left: ∀ (m n : Nat), gcd m n ∣ m
gcd_dvd_left
_: Nat
_
_: Nat
_
) (
Nat.dvd_refl: ∀ (a : Nat), a ∣ a
Nat.dvd_refl
_: Nat
_
)) @[simp] theorem
gcd_gcd_self_right_right: ∀ (m n : Nat), gcd m (gcd n m) = gcd n m
gcd_gcd_self_right_right
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
(
gcd: Nat → Nat → Nat
gcd
n: Nat
n
m: Nat
m
) =
gcd: Nat → Nat → Nat
gcd
n: Nat
n
m: Nat
m
:=

Goals accomplished! 🐙
m, n: Nat


gcd m (gcd n m) = gcd n m
m, n: Nat


gcd m (gcd n m) = gcd n m
m, n: Nat


gcd m (gcd m n) = gcd m n
m, n: Nat


gcd m (gcd n m) = gcd n m
m, n: Nat


gcd m n = gcd m n

Goals accomplished! 🐙
@[simp] theorem
gcd_gcd_self_left_right: ∀ (m n : Nat), gcd (gcd n m) m = gcd n m
gcd_gcd_self_left_right
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
(
gcd: Nat → Nat → Nat
gcd
n: Nat
n
m: Nat
m
)
m: Nat
m
=
gcd: Nat → Nat → Nat
gcd
n: Nat
n
m: Nat
m
:=

Goals accomplished! 🐙
m, n: Nat


gcd (gcd n m) m = gcd n m
m, n: Nat


gcd (gcd n m) m = gcd n m
m, n: Nat


gcd m (gcd n m) = gcd n m
m, n: Nat


gcd (gcd n m) m = gcd n m
m, n: Nat


gcd n m = gcd n m

Goals accomplished! 🐙
@[simp] theorem
gcd_gcd_self_left_left: ∀ (m n : Nat), gcd (gcd m n) m = gcd m n
gcd_gcd_self_left_left
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
(
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
)
m: Nat
m
=
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
:=

Goals accomplished! 🐙
m, n: Nat


gcd (gcd m n) m = gcd m n
m, n: Nat


gcd (gcd m n) m = gcd m n
m, n: Nat


gcd (gcd n m) m = gcd n m
m, n: Nat


gcd (gcd m n) m = gcd m n
m, n: Nat


gcd n m = gcd n m

Goals accomplished! 🐙
theorem
gcd_add_mul_self: ∀ (m n k : Nat), gcd m (n + k * m) = gcd m n
gcd_add_mul_self
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
(
n: Nat
n
+
k: Nat
k
*
m: Nat
m
) =
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
:=

Goals accomplished! 🐙
m, n, k: Nat


gcd m (n + k * m) = gcd m n

Goals accomplished! 🐙
theorem
gcd_eq_zero_iff: ∀ {i j : Nat}, gcd i j = 0 ↔ i = 0 ∧ j = 0
gcd_eq_zero_iff
{
i: Nat
i
j: Nat
j
:
Nat: Type
Nat
} :
gcd: Nat → Nat → Nat
gcd
i: Nat
i
j: Nat
j
=
0: ?m.5334
0
↔
i: Nat
i
=
0: ?m.5354
0
∧
j: Nat
j
=
0: ?m.5368
0
:= ⟨fun
h: ?m.5392
h
=> ⟨
eq_zero_of_gcd_eq_zero_left: ∀ {m n : Nat}, gcd m n = 0 → m = 0
eq_zero_of_gcd_eq_zero_left
h: ?m.5392
h
,
eq_zero_of_gcd_eq_zero_right: ∀ {m n : Nat}, gcd m n = 0 → n = 0
eq_zero_of_gcd_eq_zero_right
h: ?m.5392
h
⟩, fun
h: ?m.5414
h
=>

Goals accomplished! 🐙
i, j: Nat

h: i = 0 ∧ j = 0


gcd i j = 0

Goals accomplished! 🐙
⟩ /-! ### `lcm` -/ theorem
lcm_comm: ∀ (m n : Nat), lcm m n = lcm n m
lcm_comm
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
=
lcm: Nat → Nat → Nat
lcm
n: Nat
n
m: Nat
m
:=

Goals accomplished! 🐙
m, n: Nat


lcm m n = lcm n m
m, n: Nat


lcm m n = lcm n m
m, n: Nat


m * n / gcd m n = lcm n m
m, n: Nat


lcm m n = lcm n m
m, n: Nat


m * n / gcd m n = n * m / gcd n m
m, n: Nat


lcm m n = lcm n m
m, n: Nat


m * n / gcd m n = m * n / gcd n m
m, n: Nat


lcm m n = lcm n m
m, n: Nat


m * n / gcd m n = m * n / gcd m n

Goals accomplished! 🐙
@[simp] theorem
lcm_zero_left: ∀ (m : Nat), lcm 0 m = 0
lcm_zero_left
(
m: Nat
m
:
Nat: Type
Nat
) :
lcm: Nat → Nat → Nat
lcm
0: ?m.5514
0
m: Nat
m
=
0: ?m.5523
0
:=

Goals accomplished! 🐙
m: Nat


lcm 0 m = 0

Goals accomplished! 🐙
@[simp] theorem
lcm_zero_right: ∀ (m : Nat), lcm m 0 = 0
lcm_zero_right
(
m: Nat
m
:
Nat: Type
Nat
) :
lcm: Nat → Nat → Nat
lcm
m: Nat
m
0: ?m.5650
0
=
0: ?m.5659
0
:=

Goals accomplished! 🐙
m: Nat


lcm m 0 = 0

Goals accomplished! 🐙
@[simp] theorem
lcm_one_left: ∀ (m : Nat), lcm 1 m = m
lcm_one_left
(
m: Nat
m
:
Nat: Type
Nat
) :
lcm: Nat → Nat → Nat
lcm
1: ?m.5782
1
m: Nat
m
=
m: Nat
m
:=

Goals accomplished! 🐙
m: Nat


lcm 1 m = m

Goals accomplished! 🐙
@[simp] theorem
lcm_one_right: ∀ (m : Nat), lcm m 1 = m
lcm_one_right
(
m: Nat
m
:
Nat: Type
Nat
) :
lcm: Nat → Nat → Nat
lcm
m: Nat
m
1: ?m.5904
1
=
m: Nat
m
:=

Goals accomplished! 🐙
m: Nat


lcm m 1 = m

Goals accomplished! 🐙
@[simp] theorem
lcm_self: ∀ (m : Nat), lcm m m = m
lcm_self
(
m: Nat
m
:
Nat: Type
Nat
) :
lcm: Nat → Nat → Nat
lcm
m: Nat
m
m: Nat
m
=
m: Nat
m
:=

Goals accomplished! 🐙
m: Nat


lcm m m = m
m: Nat


lcm m m = m
m: Nat

h: m = 0


lcm m m = m
m: Nat


lcm m m = m
m: Nat

h: m = 0


lcm m m = m
m: Nat

h: m = 0


lcm 0 0 = 0
m: Nat

h: m = 0


lcm m m = m
m: Nat

h: m = 0


0 = 0

Goals accomplished! 🐙
m: Nat


lcm m m = m
m: Nat

h: m > 0


lcm m m = m
m: Nat


lcm m m = m

Goals accomplished! 🐙
theorem
dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
m: Nat
m
∣
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
:= ⟨
n: Nat
n
/
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
,

Goals accomplished! 🐙
m, n: Nat


lcm m n = m * (n / gcd m n)
m, n: Nat


lcm m n = m * (n / gcd m n)
m, n: Nat


lcm m n = m * n / gcd m n
m, n: Nat


lcm m n = m * n / gcd m n
m, n: Nat


lcm m n = m * n / gcd m n
m, n: Nat


lcm m n = m * (n / gcd m n)

Goals accomplished! 🐙
⟩ theorem
dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
n: Nat
n
∣
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
:=
lcm_comm: ∀ (m n : Nat), lcm m n = lcm n m
lcm_comm
n: Nat
n
m: Nat
m
▸
dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left
n: Nat
n
m: Nat
m
theorem
gcd_mul_lcm: ∀ (m n : Nat), gcd m n * lcm m n = m * n
gcd_mul_lcm
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
gcd: Nat → Nat → Nat
gcd
m: Nat
m
n: Nat
n
*
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
=
m: Nat
m
*
n: Nat
n
:=

Goals accomplished! 🐙
m, n: Nat


gcd m n * lcm m n = m * n
m, n: Nat


gcd m n * lcm m n = m * n
m, n: Nat


gcd m n * (m * n / gcd m n) = m * n
m, n: Nat


gcd m n * lcm m n = m * n
m, n: Nat


m * n = m * n

Goals accomplished! 🐙
theorem
lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd
{
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
} (
H1: m ∣ k
H1
:
m: Nat
m
∣
k: Nat
k
) (
H2: n ∣ k
H2
:
n: Nat
n
∣
k: Nat
k
) :
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
∣
k: Nat
k
:=

Goals accomplished! 🐙
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0


lcm m n ∣ 0
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0


lcm m n ∣ 0
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0


lcm m n ∣ 0
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

h: k = 0


lcm m n ∣ k

Goals accomplished! 🐙
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


gcd m n * lcm m n ∣ gcd m n * k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


lcm m n ∣ k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


gcd m n * lcm m n ∣ gcd m n * k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


m * n ∣ gcd m n * k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


gcd m n * lcm m n ∣ gcd m n * k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


m * n ∣ gcd (m * k) (n * k)
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


gcd m n * lcm m n ∣ gcd m n * k
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


m * n ∣ gcd (m * k) (k * n)
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


m * n ∣ gcd (m * k) (k * n)
m, n, k: Nat

H1: m ∣ k

H2: n ∣ k

kpos: k > 0


lcm m n ∣ k

Goals accomplished! 🐙
theorem
lcm_assoc: ∀ (m n k : Nat), lcm (lcm m n) k = lcm m (lcm n k)
lcm_assoc
(
m: Nat
m
n: Nat
n
k: Nat
k
:
Nat: Type
Nat
) :
lcm: Nat → Nat → Nat
lcm
(
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
)
k: Nat
k
=
lcm: Nat → Nat → Nat
lcm
m: Nat
m
(
lcm: Nat → Nat → Nat
lcm
n: Nat
n
k: Nat
k
) :=
dvd_antisymm: ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
dvd_antisymm
(
lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd
(
lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd
(
dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left
m: Nat
m
(
lcm: Nat → Nat → Nat
lcm
n: Nat
n
k: Nat
k
)) (
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left
n: Nat
n
k: Nat
k
) (
dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right
m: Nat
m
(
lcm: Nat → Nat → Nat
lcm
n: Nat
n
k: Nat
k
)))) (
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right
n: Nat
n
k: Nat
k
) (
dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right
m: Nat
m
(
lcm: Nat → Nat → Nat
lcm
n: Nat
n
k: Nat
k
)))) (
lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd
(
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left
m: Nat
m
n: Nat
n
) (
dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left
(
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
)
k: Nat
k
)) (
lcm_dvd: ∀ {m n k : Nat}, m ∣ k → n ∣ k → lcm m n ∣ k
lcm_dvd
(
Nat.dvd_trans: ∀ {a b c : Nat}, a ∣ b → b ∣ c → a ∣ c
Nat.dvd_trans
(
dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right
m: Nat
m
n: Nat
n
) (
dvd_lcm_left: ∀ (m n : Nat), m ∣ lcm m n
dvd_lcm_left
(
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
)
k: Nat
k
)) (
dvd_lcm_right: ∀ (m n : Nat), n ∣ lcm m n
dvd_lcm_right
(
lcm: Nat → Nat → Nat
lcm
m: Nat
m
n: Nat
n
)
k: Nat
k
))) theorem
lcm_ne_zero: ∀ {m n : Nat}, m ≠ 0 → n ≠ 0 → lcm m n ≠ 0
lcm_ne_zero
(
hm: m ≠ 0
hm
:
m: ?m.6758
m
≠
0: ?m.6784
0
) (
hn: n ≠ 0
hn
:
n: ?m.6778
n
≠
0: ?m.6798
0
) :
lcm: Nat → Nat → Nat
lcm
m: ?m.6758
m
n: ?m.6778
n
≠
0: ?m.6812
0
:=

Goals accomplished! 🐙
m, n: Nat

hm: m ≠ 0

hn: n ≠ 0


lcm m n ≠ 0
m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0


lcm m n ≠ 0
m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * lcm m n = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0


lcm m n ≠ 0
m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * lcm m n = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * 0 = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: gcd m n * lcm m n = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0


lcm m n ≠ 0
m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

hm1: m = 0


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n



Goals accomplished! 🐙
m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n

hn1: n = 0


m, n: Nat

hm: m ≠ 0

hn: n ≠ 0

h: lcm m n = 0

h1: 0 = m * n



Goals accomplished! 🐙
/-! ### `coprime` See also `nat.coprime_of_dvd` and `nat.coprime_of_dvd'` to prove `nat.coprime m n`. -/
instance: (m n : Nat) → Decidable (coprime m n)
instance
(
m: Nat
m
n: Nat
n
:
Nat: Type
Nat
) :
Decidable: Prop → Type
Decidable
(
coprime: Nat → Nat → Prop
coprime
m: Nat
m
n: Nat
n
) :=
inferInstanceAs: (α : Sort ?u.7015) → [i : α] → α
inferInstanceAs
(
Decidable: Prop → Type
Decidable
(
_: ?m.7018
_
=
1: ?m.7021
1
)) theorem
coprime_iff_gcd_eq_one: ∀ {m n : Nat}, coprime m n ↔ gcd m n = 1
coprime_iff_gcd_eq_one
:
coprime: Nat → Nat → Prop
coprime
m: ?m.7130
m
n: ?m.7134
n
↔
gcd: Nat → Nat → Nat
gcd
m: ?m.7130
m
n: ?m.7134
n
=
1: ?m.7139
1
:=
.rfl: ∀ {a : Prop}, a ↔ a
.rfl
theorem
coprime.gcd_eq_one: ∀ {m n : Nat}, coprime m n → gcd m n = 1
coprime.gcd_eq_one
:
coprime: Nat → Nat → Prop
coprime
m: ?m.7168
m
n: ?m.7173
n
→
gcd: Nat → Nat → Nat
gcd
m: ?m.7168
m
n: ?m.7173
n
=
1: ?m.7180
1
:=
id: ∀ {α : Sort ?u.7201}, α → α
id
theorem
coprime.symm: ∀ {n m : Nat}, coprime n m → coprime m n
coprime.symm
:
coprime: Nat → Nat → Prop
coprime
n: ?m.7211
n
m: ?m.7216
m
→
coprime: Nat → Nat → Prop
coprime
m: ?m.7216
m
n: ?m.7211
n
:= (
gcd_comm: ∀ (m n : Nat), gcd m n = gcd n m
gcd_comm
m: Nat
m
n: Nat
n
).
trans: ∀ {α : Sort ?u.7227} {a b c : α}, a = b → b = c → a = c
trans
theorem
coprime_comm: ∀ {n m : Nat}, coprime n m ↔ coprime m n
coprime_comm
:
coprime: Nat → Nat → Prop
coprime
n: ?m.7248
n
m: ?m.7252
m
↔
coprime: Nat → Nat → Prop
coprime
m: ?m.7252
m
n: ?m.7248
n
:= ⟨
coprime.symm: ∀ {n m : Nat}, coprime n m → coprime m n
coprime.symm
,
coprime.symm: ∀ {n m : Nat}, coprime n m → coprime m n
coprime.symm
⟩ theorem
coprime.dvd_of_dvd_mul_right: ∀ {k n m : Nat}, coprime k n → k ∣ m * n → k ∣ m
coprime.dvd_of_dvd_mul_right
(
H1: coprime k n
H1
:
coprime: Nat → Nat → Prop
coprime
k: ?m.7282
k
n: ?m.7286
n
) (
H2: k ∣ m * n
H2
:
k: ?m.7282
k
∣
m: ?m.7300
m
*
n: ?m.7286
n
) :
k: ?m.7282
k
∣
m: ?m.7300
m
:=

Goals accomplished! 🐙
k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n


k ∣ m
k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ∣ gcd (m * k) (m * n)


k ∣ m
k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n


k ∣ m
k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ∣ gcd (m * k) (m * n)


k ∣ m
k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t: k ∣ m * gcd k n


k ∣ m
k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t:= dvd_gcd (Nat.dvd_mul_left k m) H2: k ∣ gcd (m * k) (m * n)


k ∣ m
k, n, m: Nat

H1: coprime k n

H2: k ∣ m * n

t: k ∣ m * 1


k ∣ m
k, n, m: Nat

H1: coprime k n

H2: