OAI/NumberTheory/DukePrimeDegree/Geometry/RootRowShear.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Conjugation by the next root is the product of its row shears

  1. abbrev OAI.DukePrimeDegree.InitialRootStep.NextRoot line 16
  2. def OAI.DukePrimeDegree.InitialRootStep.rowTargets line 18
  3. lemma OAI.DukePrimeDegree.InitialRootStep.row_source_mem line 21
  4. def OAI.DukePrimeDegree.InitialRootStep.rowSource line 44
  5. lemma OAI.DukePrimeDegree.InitialRootStep.rowSource_val line 47
  6. lemma OAI.DukePrimeDegree.InitialRootStep.rowSource_not_target line 50
  7. def OAI.DukePrimeDegree.InitialRootStep.rowShear line 57
  8. lemma OAI.DukePrimeDegree.InitialRootStep.rowShear_apply line 60
  9. lemma OAI.DukePrimeDegree.InitialRootStep.rowShear_eq_conjugation_entries line 70