Documentation

Init.Data.Nat.Gcd

@[extern lean_nat_gcd]
def Nat.gcd (a : Nat) (b : Nat) :
Instances For
    @[simp]
    theorem Nat.gcd_zero_left (y : Nat) :
    Nat.gcd 0 y = y
    theorem Nat.gcd_succ (x : Nat) (y : Nat) :
    @[simp]
    theorem Nat.gcd_one_left (n : Nat) :
    Nat.gcd 1 n = 1
    @[simp]
    theorem Nat.gcd_zero_right (n : Nat) :
    Nat.gcd n 0 = n
    @[simp]
    theorem Nat.gcd_self (n : Nat) :
    Nat.gcd n n = n