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>
