The Chevalley-Warning Theorem

This development formalizes the Chevalley--Warning theorem for finite fields: if finitely many multivariate polynomials over a finite field have total degree sum strictly smaller than the number of variables, then the number of their common zeros is divisible by the characteristic. Polynomials are represented by finite sparse term lists, and the proof follows the standard finite-field power-sum argument. AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle