OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockGauss.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual two-block Gauss coordinates in the special linear group

An invertible principal block gives lower-cross, neutral, and upper-cross factors. The neutral factor is constructed by multiplication inside SL, so no separate determinant formula is postulated. These are the algebraic coordinates for the singular-block chart; topology and conditional graph transport are subsequent steps.

  1. def OAI.DukePrimeDegree.twoBlockUpperCoordinate line 21
  2. def OAI.DukePrimeDegree.twoBlockLowerCoordinate line 25
  3. def OAI.DukePrimeDegree.twoBlockCore line 29
  4. theorem OAI.DukePrimeDegree.twoBlockGauss_factorization line 33
  5. theorem OAI.DukePrimeDegree.twoBlockCore_matrix line 39
  6. theorem OAI.DukePrimeDegree.twoBlockCore_mem_neutral line 62
  7. lemma OAI.DukePrimeDegree.isUnit_principal_of_twoBlockNeutral line 68
  8. lemma OAI.DukePrimeDegree.twoBlock_product_matrix line 80
  9. theorem OAI.DukePrimeDegree.twoBlockGauss_coordinates_product line 97
  10. lemma OAI.DukePrimeDegree.twoBlock_product_principal_isUnit line 111
  11. theorem OAI.DukePrimeDegree.twoBlockCore_product line 118