OAI/NumberTheory/DukePrimeDegree/Geometry/RowTimeSplit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Separating one coordinate of the abelian row group

The row time space splits into the kernel of one coordinate and that real coordinate. Under the row-group parametrization, the final factor is exactly the corresponding elementary root transvection.

  1. def OAI.DukePrimeDegree.rowUnit line 20
  2. lemma OAI.DukePrimeDegree.rowUnit_apply_self line 25
  3. def OAI.DukePrimeDegree.rowRemainingTimeSpace line 28
  4. abbrev OAI.DukePrimeDegree.RowRemainingTime line 31
  5. lemma OAI.DukePrimeDegree.rowRemainingTime_self line 33
  6. def OAI.DukePrimeDegree.rowTimeSplit line 36
  7. lemma OAI.DukePrimeDegree.rowRoot_smul_unit line 59
  8. lemma OAI.DukePrimeDegree.rowRoot_split line 76