Gröbner Bases of Modules and Faugère's $F_4$ Algorithm in Isabelle/HOL

Alexander Maletzky, Fabian Immler

We present an elegant, generic and extensive formalization of Gröbner bases in Isabelle/HOL. The formalization covers all of the essentials of the theory (polynomial reduction, S-p…