OAI/NumberTheory/DukePrimeDegree/Geometry/EliminationRootOrder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Every positive root occurs exactly once

The chart compatibility conditions prohibit repeating an eliminated root: a repeat would force an eliminated diagonal entry. A complete chain therefore lists exactly the positive roots, without repetitions.

  1. def OAI.DukePrimeDegree.EliminationChain.roots line 21
  2. lemma OAI.DukePrimeDegree.EliminationChain.finalEntries_eq_union_roots line 26
  3. lemma OAI.DukePrimeDegree.EliminationChain.roots_notMem_initial line 34
  4. lemma OAI.DukePrimeDegree.EliminationChain.roots_nodup line 49
  5. lemma OAI.DukePrimeDegree.completeRootChain_roots_toFinset line 60
  6. lemma OAI.DukePrimeDegree.completeRootChain_roots_nodup line 65
  7. lemma OAI.DukePrimeDegree.completeRootChain_roots_length line 71