OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockGaussChart.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The open two-block Gauss chart

The cell with invertible principal block is homeomorphic to lower-cross coordinates times the actual neutral subgroup times upper-cross coordinates. This is a concrete parabolic chart, independent of the lexicographic initial-segment root coordinates.

  1. def OAI.DukePrimeDegree.twoBlockGaussCell line 21
  2. abbrev OAI.DukePrimeDegree.TwoBlockGaussCoordinates line 24
  3. def OAI.DukePrimeDegree.twoBlockGaussEquiv line 27
  4. lemma OAI.DukePrimeDegree.isOpen_twoBlockGaussCell line 42
  5. lemma OAI.DukePrimeDegree.one_mem_twoBlockGaussCell line 50
  6. lemma OAI.DukePrimeDegree.continuous_twoBlockUpper line 55
  7. lemma OAI.DukePrimeDegree.continuous_twoBlockLower line 66
  8. lemma OAI.DukePrimeDegree.continuous_twoBlockPrincipalInverse line 77
  9. lemma OAI.DukePrimeDegree.continuous_twoBlockGaussEquiv line 91
  10. lemma OAI.DukePrimeDegree.continuous_twoBlockGaussEquiv_symm line 109
  11. def OAI.DukePrimeDegree.twoBlockGaussHomeomorph line 116