Rationality of the zeta function (Dwork)

Let $k=\mathbb F_q$ be a finite field with $q$ elements, of characteristic $p$, and let $X$ be a non-singular projective variety of dimension $n$ over $k$, i.e. $f: X\to\operatorname{Spec}k$ is smooth of relative dimension $n$, geometrically irreducible and projective. Let $N_m=\#X(\mathbb F_{q^m})$ and $Z(X,T)=\exp\big(\sum_{m\ge1}N_mT^m/m\big)\in\mathbb Q[[T]]$. Then $Z(X,T)$ is a rational function of $T$: there are polynomials $P,Q\in\mathbb Q[T]$ with $Q\ne0$ and

This is the first part of the Weil conjectures to be proved, by Dwork in 1960 using $p$-adic methods.

Formalization Note The finite field is a type k with [Field k] [Finite k] [CharP k p], $q$ = Nat.card k; $\mathbb F_{q^m}$ is FiniteField.Extension k p m; $N_m$ counts $k$-morphisms $\operatorname{Spec}\mathbb F_{q^m}\to X$; $Z(X,T)$ is zetaFunction p f. Projectivity is a closed immersion into projectiveSpace k N over $k$.