OAI/NumberTheory/DukePrimeDegree/Geometry/OrderedEliminationChain.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Existence of the complete ordered elimination chain

At each step choose the least remaining positive root in row order. The processed roots form an initial segment, which proves exactly the zero-preservation and pivot conditions required by the next chart.

  1. def OAI.DukePrimeDegree.allPositiveRoots line 20
  2. def OAI.DukePrimeDegree.InitialRootPattern line 23
  3. def OAI.DukePrimeDegree.PivotsFromPattern line 27
  4. lemma OAI.DukePrimeDegree.initialRootPattern_stable line 30
  5. lemma OAI.DukePrimeDegree.initialRootPattern_pivot_notMem line 46
  6. lemma OAI.DukePrimeDegree.initialRootPattern_insert_min line 56
  7. lemma OAI.DukePrimeDegree.pivotsFromPattern_insert line 70
  8. theorem OAI.DukePrimeDegree.exists_complete_elimination_chain line 79