Exact edge accounting for finite matching decompositions

The equivalence on individual edges yields an exact count, including palettes with unused colours. Only the edge set must be finite: infinitely many isolated vertices are allowed. Empty matching classes contribute zero.

theorem SimpleGraph.MatchingDecomposition.card_edges_eq_sum {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} [Finite ↑G.edgeSet] [Fintype C] (D : G.MatchingDecomposition C) : Nat.card ↑G.edgeSet = ∑ c : C, Nat.card ↑(D.matching c).edgeSet

The total number of edges is the sum of the matching-class sizes.