OAI/NumberTheory/DukePrimeDegree/Geometry/ConjugationRestrictions.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalized restrictions under extremal conjugation

  1. def OAI.DukePrimeDegree.InitialRootStep.nextConjugationHomeomorph line 13
  2. lemma OAI.DukePrimeDegree.InitialRootStep.map_normalized_restriction_conjugation line 23