Formalizing Hall's Marriage Theorem in Lean

Alena Gusakov, Bhavik Mehta, Kyle A. Miller

We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, which is a community-driven effort to build a unified mathematics library for Lean. One go…