Documentation

FormalConjecturesForMathlib.Combinatorics.SimpleGraph.SpanningTree

noncomputable def SimpleGraph.Ls {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] :

Ls G is the maximum number of leaves over all spanning trees of G. It is defined to be 0 when G is not connected.

Equations
  • One or more equations did not get rendered due to their size.
Instances For