OAI/NumberTheory/DukePrimeDegree/Geometry/LexicographicRootWeights.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Neutral weights for every lexicographic elimination step

The least remaining root can be kept neutral while all other remaining root directions contract. Thus the actual Gaussian elimination order has the weights needed by the conditional product induction.

  1. def OAI.DukePrimeDegree.lexicographicNeutralRaw line 19
  2. lemma OAI.DukePrimeDegree.lexicographicNeutralRaw_equal line 22
  3. lemma OAI.DukePrimeDegree.lexicographicNeutralRaw_strict line 26
  4. theorem OAI.DukePrimeDegree.exists_lexicographic_root_weights line 54
  5. lemma OAI.DukePrimeDegree.initialRemaining_roots_closed line 68
  6. lemma OAI.DukePrimeDegree.initialRemaining_erase line 82