### Abstract

We implement the Babylonian method to compute n-th roots of numbers. We provide precise algorithms for naturals, integers and rationals, and offer an approximation algorithm for square roots over linear ordered fields. Moreover, there are precise algorithms to compute the floor and the ceiling of n-th roots.

### License

GNU Lesser General Public License (LGPL)

### History

July 11, 2014
  Moved NthRoot_Impl from Real-Impl to this entry.
October 16, 2013
  Added algorithms to compute floor and ceiling of sqrt of integers.

### Topics

- Mathematics/Analysis

### Session Sqrt_Babylonian

- Sqrt_Babylonian_Auxiliary
- Log_Impl
- NthRoot_Impl
- Sqrt_Babylonian

### Depends on

- Cauchy’s Mean Theorem and the Cauchy-Schwarz Inequality

### Used by

- Polynomial Factorization
- Polynomial Interpolation
- QR Decomposition
- Implementing field extensions of the form Q[sqrt(b)]

### Auto-related entries

- Factorization of Polynomials with Algebraic Coefficients

## Cite

×

Sqrt_Babylonian-AFP

    @article{Sqrt_Babylonian-AFP,
      author  = {René Thiemann},
      title   = {Computing N-th Roots using the Babylonian Method},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Sqrt_Babylonian.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- Jan 4, 2013 : Isabelle2012