Documentation

Mathlib.Init.Data.Nat.GCD

Definitions and properties of gcd, lcm, and coprime #

gcd

source
ink
theorem Nat.gcd_def (x : ℕ) (y : ℕ) :
Nat.gcd x y = if x = 0 then y else Nat.gcd (y % x) x