OAI/NumberTheory/DukePrimeDegree/Geometry/RootSourceOrder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A root graph without two consecutive edges admits a source ordering

  1. theorem OAI.DukePrimeDegree.exists_source_order line 15

    Source documentation

    Put targets before sources. This is the only finite ordering fact needed when the commutator theorem rules out two consecutive positive roots.

    theorem exists_source_order (n : ℕ) (r : Fin n → Fin n → Prop)
    (hchain : ∀ a b c, r a b → r b c → False) :
    ∃ e : Equiv.Perm (Fin n), ∀ i j, r i j → e j < e i := by
…