OAI/NumberTheory/DukePrimeDegree/Geometry/NextGroupConjugation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conjugation preserves the intrinsic product on the actual next subgroup

  1. lemma OAI.DukePrimeDegree.InitialRootStep.next_conjugation_mem line 13
  2. def OAI.DukePrimeDegree.InitialRootStep.nextConjugation line 29
  3. lemma OAI.DukePrimeDegree.InitialRootStep.continuous_nextConjugation line 35
  4. lemma OAI.DukePrimeDegree.InitialRootStep.nextConjugation_coordinates line 39
  5. def OAI.DukePrimeDegree.InitialRootStep.nextIntrinsicProduct line 51
  6. theorem OAI.DukePrimeDegree.ae_nextIntrinsicProduct_conjugation line 60