OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingRootCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Global coordinates on each remaining Gaussian root subgroup

  1. def OAI.DukePrimeDegree.EliminationChain.identityFinal line 17
  2. lemma OAI.DukePrimeDegree.EliminationChain.word_mem_remaining line 30
  3. theorem OAI.DukePrimeDegree.EliminationChain.word_surjective_remaining line 43
  4. theorem OAI.DukePrimeDegree.EliminationChain.word_isEmbedding_remaining line 71
  5. def OAI.DukePrimeDegree.EliminationChain.remainingWordMap line 81
  6. theorem OAI.DukePrimeDegree.EliminationChain.remainingWordMap_isEmbedding line 86
  7. theorem OAI.DukePrimeDegree.EliminationChain.remainingWordMap_surjective line 91
  8. def OAI.DukePrimeDegree.EliminationChain.remainingWordHomeomorph line 98
  9. lemma OAI.DukePrimeDegree.EliminationChain.remainingWordHomeomorph_apply line 104