OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingEuclideanCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Matrix-entry coordinates on every remaining Gaussian subgroup

  1. lemma OAI.DukePrimeDegree.EliminationChain.roots_toFinset_remaining line 15
  2. def OAI.DukePrimeDegree.EliminationChain.remainingIndexEquiv line 33
  3. def OAI.DukePrimeDegree.EliminationChain.remainingEuclideanCoordinates line 45
  4. lemma OAI.DukePrimeDegree.EliminationChain.remainingEuclideanCoordinates_entry line 50
  5. def OAI.DukePrimeDegree.EliminationChain.remainingGroupCoordinates line 64
  6. lemma OAI.DukePrimeDegree.EliminationChain.remainingGroupCoordinates_apply line 69