OAI/NumberTheory/DukePrimeDegree/Geometry/EliminationWordEntries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Gaussian word coordinates are the actual upper matrix entries

  1. lemma OAI.DukePrimeDegree.EliminationChain.word_column_of_pivot line 16
  2. lemma OAI.DukePrimeDegree.EliminationChain.word_step_add_single line 28
  3. theorem OAI.DukePrimeDegree.EliminationChain.word_val_eq_sum_single line 45