no goals
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype V
h : IsPerfectMatching M
⊢ Even (Fintype.card V)
classical
simpa only [h.2.card_verts] using IsMatching.even_card h.1
no goals
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype V
h : IsPerfectMatching M
⊢ Even (Fintype.card V)
simpa only [h.2.card_verts] using IsMatching.even_card h.1