Graph theory def: Matching number

[SnirBroshi]

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.

[JTylM]

Do you think, this is a good first issue? If so could you assign me?