Documentation

Init.Data.Nat.Sqrt.Basic

source
def Nat.sqrt (n : Nat) :
Nat

Integer square root function. Implemented via Newton's method.

Instances For
    source
    @[irreducible]
    def Nat.sqrt.iter (n guess : Nat) :
    Nat

    Auxiliary for sqrt. If guess is greater than the integer square root of n, returns the integer square root of n.

    Instances For