OAI/NumberTheory/DukePrimeDegree/Geometry/EliminationChain.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Composing Gaussian root-coordinate charts

A finite sequence of compatible eliminations gives an actual open embedding of the final transverse slice and all its real root coordinates. Its parametrization is multiplication by the ordered product of the elementary root matrices.

  1. inductive OAI.DukePrimeDegree.EliminationChain line 21
  2. def OAI.DukePrimeDegree.EliminationChain.finalEntries line 32
  3. def OAI.DukePrimeDegree.EliminationChain.finalPivots line 37
  4. theorem OAI.DukePrimeDegree.EliminationChain.entries_subset_final line 42
  5. def OAI.DukePrimeDegree.EliminationChain.Time line 48
  6. instance OAI.DukePrimeDegree.EliminationChain.timeTopology line 53
  7. abbrev OAI.DukePrimeDegree.EliminationChain.FinalSlice line 58
  8. def OAI.DukePrimeDegree.EliminationChain.param line 61
  9. theorem OAI.DukePrimeDegree.EliminationChain.param_isOpenEmbedding line 68
  10. def OAI.DukePrimeDegree.EliminationChain.word line 77
  11. theorem OAI.DukePrimeDegree.EliminationChain.param_val line 83
  12. def OAI.DukePrimeDegree.EliminationChain.zeroTime line 95
  13. theorem OAI.DukePrimeDegree.EliminationChain.word_zeroTime line 100
  14. theorem OAI.DukePrimeDegree.EliminationChain.param_zeroTime line 107
  15. theorem OAI.DukePrimeDegree.EliminationChain.word_mem_generated line 111