Theorem SimpleGraph.exists_bijective_of_forall_ncard_le

Modification history

2025-11-04 06:00
Mathlib/Combinatorics/SimpleGraph/Hall.lean
feat(SimpleGraph): Hall's Marriage Theorem for bipartite graphs (#29164) …
Added SimpleGraph.exists_bijective_of_forall_ncard_leView on Github →