Theorem SimpleGraph.exists_isMatching_of_forall_ncard_le

Modification history

2025-11-20 07:16
Mathlib/Combinatorics/SimpleGraph/Hall.lean
chore: remove unused `Decidable*` instances in theorem types (#31831) …
Modified SimpleGraph.exists_isMatching_of_forall_ncard_leView on Github →
2025-11-04 06:00
Mathlib/Combinatorics/SimpleGraph/Hall.lean
feat(SimpleGraph): Hall's Marriage Theorem for bipartite graphs (#29164) …
Added SimpleGraph.exists_isMatching_of_forall_ncard_leView on Github →