leanprover-community / leanprover-community/mathlib4
Graph theory def: Matching number
Open
Nobody has claimed this yet.
help-wanted
t-combinatorics
- Dominant language
- Lean
- Stars
- 4.2k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
Matchings in simple graphs exist as SimpleGraph.Subgraph.IsMatching.
I suggest we're missing the following def for the matching number of a simple graph:
noncomputable def matchingNumber (G : SimpleGraph V) : ℕ∞ :=
⨆ (M : G.Subgraph) (_ : M.IsMatching), M.edgeSet.encard
and basic API for it.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.