feat(combinatorics/hall): Hall's marriage theorem (#5695)

We state and prove Hall's marriage theorem with respect to fintypes and relations. 

Coauthor: @b-mehta @kmill



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>

Author: agusakov

docs/references.bib

@@ -545,6 +545,28 @@ @misc{scholze2011perfectoid
       primaryClass={math.AG}
 }
 
+@Article{Hall1935,
+  author    = {P. Hall},
+  journal   = {Journal of the London Mathematical Society},
+  title     = {On Representatives of Subsets},
+  year      = {1935},
+  month     = {jan},
+  number    = {1},
+  pages     = {26--30},
+  volume    = {s1-10},
+  doi       = {10.1112/jlms/s1-10.37.26},
+  publisher = {Wiley}
+}
+
+@Article{Gusakov2021,
+  author      = {Alena Gusakov and Bhavik Mehta and Kyle A. Miller},
+  title       = {Formalizing Hall's Marriage Theorem in Lean},
+  eprint      = {2101.00127},
+  eprintclass = {math.CO},
+  eprinttype  = {arXiv},
+  keywords    = {math.CO, cs.LO, 05-04 (Primary) 05C70, 68R05 (Secondary)},
+}
+
 @book {MR1237403,
     AUTHOR = {Lidl, R. and Mullen, G. L. and Turnwald, G.},
      TITLE = {Dickson polynomials},