We give an explicit construction of an integral basis for a radical function field $K=k(t,\rho )$, where ${\rho }^n=D\in k\left[t\right]$, under the assumptions $[K:k(t\left)\right]=n$ and $char\left(k\right)\nmid n$. The field discriminant of $K$ is also computed. We explain why these questions are substantially easier than the corresponding ones in number fields. Some formulae for the $P$-signatures of a radical function field are also discussed in this paper.

We prove that $|{\sum }_{d\le x,(d,q)=1}\mu \left(d\right)/d|\le 2.4(q/\phi \left(q\right))/log(x/q)$ for every x > q ≥ 1, and similar estimates for the Liouville function. We also give better constants when x/q is large.,

Let χ be a primitive Dirichlet character of conductor q and denote by L(z,χ) the associated L-series. We provide an explicit upper bound for |L(1,χ)| when 3 divides q.

In this article we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm [9]. Besides the a gcd b, Extended Euclidean Algorithm can calculate a pair of two integers (x, y) that holds ax + by = a gcd b. In addition, we formalize an algorithm that can compute a solution of the Chinese remainder theorem by using Extended Euclidean Algorithm. Our aim is to support the implementation of number theoretic tools. Our formalization of those algorithms is based...