Buchberger formalization artifact

This root module imports the exact Mathlib modules discussed in the companion paper. Their source is supplied by the pinned Sanghyeok0/mathlib4 dependency.