Main.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HadwigerMatching.full_matching_minor_proposition line 12
Source documentation
The matching–minor proposition: the Hadwiger bound and its chromatic consequence when the independence and touching-matching numbers are small.
```
theorem full_matching_minor_proposition
    (V : Type) [Fintype V] [Nonempty V] (G : SimpleGraph V) :
    let m : ℕ := Fintype.card V
…
```