Documentation
Mathlib
.
Init
.
Data
.
Nat
.
GCD
Search
Google site search
Mathlib
.
Init
.
Data
.
Nat
.
GCD
source
Imports
Init
Mathlib.Init.Meta.WellFoundedTactics
Mathlib.Init.Data.Nat.Lemmas
Imported by
Nat
.
gcd_def
Definitions and properties of gcd, lcm, and coprime
#
gcd
source
theorem
Nat
.
gcd_def
(x :
ℕ
)
(y :
ℕ
)
:
Nat.gcd
x
y
=
if
x
=
0
then
y
else
Nat.gcd
(
y
%
x
)
x