Let \(K\) be a number field of degree \(d\), let \(\sigma \colon K\to \mathbb {C}\) be a field embedding, and let \(\alpha \in K\), \(\alpha \neq 0\). If \(c\alpha \) is an algebraic integer for some integer \(c\neq 0\), then

Source: Standard (Liouville’s inequality).

Let \(K\) be a number field and \((\theta _i)_{i\in I}\) a finite family in \(K\). There are a non-zero algebraic integer \(b\in K\) and a real number \(H\ge 1\) such that for every \(e\in \mathbb {N}^{I}\) and every \(E\in \mathbb {N}\) with \(\sum _ie_i\le E\), the number \(b^{E}\prod _i\theta _i^{e_i}\) is an algebraic integer whose house is at most \(H^{E}\).

Source: Standard.

Let \(K\) be a field of characteristic zero and let \(\alpha \in K\) be algebraic over \(\mathbb {Q}\). There are \(\ell ,A\in \mathbb {N}\) and an integer \(L\neq 0\) such that for every \(n\in \mathbb {N}\) there are integers \(r_0,\dots ,r_{\ell -1}\) with \(|r_l|\le A^{n}\) and

Source: Standard.

Let \(u\in \mathbb {C}\) with \(e^{u}\) algebraic, and let \(a\in \mathbb {Q}\). Then \(e^{au}\) is algebraic.

Source: Standard.

Let \(A\) be an \(m\times n\) matrix with integer entries, where \(n\ge 1\) and \(2m\le n\), and suppose that every entry satisfies \(|A_{ab}|\le B\) for some real \(B\ge 1\). Then there is \(t\in \mathbb {Z}^{n}\), \(t\neq 0\), with \(At=0\) and \(|t_b|\le nB\) for every \(b\).

Source: Siegel’s lemma [ Lang66 , Ch. I, § 2 ] , in the form Mathlib states it for integer matrices.

Let \(\omega _1,\dots ,\omega _l\in \mathbb {C}\) be pairwise distinct, let \(q_1,\dots ,q_l\in \mathbb {N}\), and let \(b_{j,i}\in \mathbb {C}\) (\(1\le j\le l\), \(0\le i\lt q_j\)) be not all zero. Then the function

takes a non-zero value at some point of \(\mathbb {C}\).

Source: Classical; see [ Tij71 ] or [ Wal71 , § 4 ] .

Let \(F(z)=\sum _{i\in I}c_ie^{\rho _iz}\) be a finite exponential sum with pairwise distinct \(\rho _i\in \mathbb {C}\) and coefficients \(c_i\in \mathbb {C}\) not all zero. Let \(m\ge 1\) and \(n\in \mathbb {N}\), and suppose that \(F^{(k)}(j)=0\) for all \(j\in \{ 1,\dots ,m\} \) and \(k\lt n\). Then there are \(r\ge n\) and \(l_0\in \{ 1,\dots ,m\} \) with \(F^{(r)}(l_0)\neq 0\) and \(F^{(k)}(j)=0\) for all \(j\in \{ 1,\dots ,m\} \) and \(k\lt r\).

Source: Standard.

Let \(F\) be an entire function, \(c\in \mathbb {C}\), \(\rho \ge 0\) and \(R\gt \rho +1\). Let \(S\) be a finite set of points \(z\) with \(|z-c|\le \rho \), and put \(\sigma =\sum _{z\in S}\operatorname {ord}_zF\). If \(|F(z)|\le M\) whenever \(|z-c|=R\), then for every \(s\in \mathbb {N}\)

Source: [ Wal71 , § 4, (4.3) ] .

Let \(y_1,\dots ,y_l\in \mathbb {C}\) be linearly independent over \(\mathbb {Q}\), and let \(F(z)=\sum _{k\in s}c_kz^{e_k}e^{\omega _kz}\) be a finite sum with \(|\omega _k|\le W\) and \(e_k\le E\) for all \(k\). Let \(t_j\le A_j\) (\(1\le j\le l\)) and \(n\) be natural numbers, and suppose that \(F^{(i)}\bigl(\sum _jm'_jy_j\bigr)=0\) for all \(i\lt n\) and all \(m'\in \mathbb {N}^{l}\) with \(m'_j\lt t_j\) for every \(j\). Let \(u\ge 2\) and \(Z\ge \bigl(\sum _jA_j|y_j|+1\bigr)(u+1)\). Then for every \(m\in \mathbb {N}^{l}\) with \(m_j\lt A_j\) for every \(j\), every \(r\in \mathbb {N}\) and \(w=\sum _jm_jy_j\),

Source: The analytic step of the extrapolation in [ Wal73 , Lemme 5 ] and in the six exponentials theorem [ Lang66 , Ch. II ] ; it rests on [ Wal71 , § 4, (4.3) ] .

Let \(f(z)=\sum _{j\in J}P_j(z)e^{w_jz}\), over a finite set \(J\), with \(|w_j|\le W\) for some \(W\ge 0\), and each \(P_j\in \mathbb {C}[z]\) zero or of degree less than \(q_j\); put \(N=\sum _jq_j\). Let \(c\in \mathbb {C}\) and \(D\ge 0\). If \(|f^{(s)}(c)|\le D\) for every \(s\lt N\), then

The \(w_j\) need not be distinct.

Source: No source is claimed; an elementary induction.

For every finite family \((f_i)_{i\in s}\) in \(\mathbb {Z}[X][Y]\),

Source: Standard.

For all \(P,Q\in \mathbb {Z}[X][Y]\), \(L(PQ)\le L(P)\, L(Q)\).

Source: Standard.

Let \(Q\in \mathbb {Z}[X][Y]\). There is \(C\in \mathbb {N}\) such that for all \(b,e,n\in \mathbb {N}\) and every \(P\in \mathbb {Z}[X][Y]\) with \(L(P)\le b\), every coefficient of \(X\)-degree at most \(e\), and \(Y\)-degree at most \(n\), the remainder \(P\bmod Q\) of the division by \(Q\) in \(Y\) satisfies

and every coefficient of \(P\bmod Q\) has \(X\)-degree at most \(e+Cn\). (When \(Q\) is not monic in \(Y\), the remainder is \(P\), as in Mathlib’s modByMonic.)

Source: Standard.

Let \(F,G\in \mathbb {C}[X]\) with \(M(F)\ge 1\) and \(M(G)\ge 1\). Then for every \(\theta \in \mathbb {C}\)

Source: [ RW97 , Corollary 3.7 ] , in the complex form of their Lemma 3.4; they describe the inequality as well known.

Let \(P\in \mathbb {Z}[X]\) have positive degree and let \(\theta \in \mathbb {C}\). Then \(P=Q^{e}R\) with \(Q,R\in \mathbb {Z}[X]\), \(Q\) irreducible of positive degree, \(e\ge 1\), and

Source: The multiplicative step of Gel’fond’s lemma [ Gel52 ] , as in [ Wal71 , § 3, Lemme 2 ] .

Let \(\omega \in \mathbb {C}\) be transcendental and let \(\theta \in \mathbb {C}\) be algebraic over \(\mathbb {Q}(\omega )\). There are \(\omega _1\in \mathbb {C}\) and \(Q\in \mathbb {Z}[X][Y]\), monic in \(Y\) of degree \(d\ge 1\), with \(Q(\omega ,\omega _1)=0\) and minimal there: no non-zero \(A\in \mathbb {Z}[X][Y]\) with \(\deg _YA\lt d\) vanishes at \((\omega ,\omega _1)\). Moreover \(\omega _1=v(\omega )\, \theta \) for some \(v\in \mathbb {Z}[X]\) with \(v(\omega )\neq 0\).

Source: Standard; the normalisation at the start of [ Wal73 , § III ] .

Let \(\omega \in \mathbb {C}\) be transcendental and let \((z_i)_{i\in I}\) be a finite family of complex numbers algebraic over \(\mathbb {Q}(\omega )\). There are \(\omega _1\in \mathbb {C}\) and \(Q\in \mathbb {Z}[X][Y]\), monic in \(Y\) of degree \(d\ge 1\), with \(Q(\omega ,\omega _1)=0\) and minimal there in the sense of Lemma 2.16, and \(D,E_i\in \mathbb {Z}[X][Y]\) with \(D(\omega ,\omega _1)\neq 0\) and

Source: Standard; the presentation used in [ Wal73 , § III ] .

Let \(K\subseteq L\) be fields, \(x\in L\), and \(S\subseteq L\) a set each of whose elements is algebraic over the ring \(K[x]\). Then the \(K\)-algebra \(K[S]\) generated by \(S\) has transcendence degree at most one over \(K\).

Source: Standard.

Let \(R\) be a commutative ring, \(A\) a commutative \(R\)-algebra and \(t\in A\) transcendental over \(R\). If \(t\) and \(z\in A\) are not algebraically independent over \(R\), then \(z\) is algebraic over the subalgebra \(R[t]\).

Source: Standard.