OAI/NumberTheory/DukePrimeDegree/Dynamics/TwoBlockNeutralAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The neutral action on a cross-block root group

The actual block-diagonal subgroup normalizes the upper cross-block group. We keep the matrix action explicit, so reordering the Gauss chart will put the neutral factor last and expose actual right-translation covariance.

  1. lemma OAI.DukePrimeDegree.twoBlockNeutral_matrix line 19
  2. lemma OAI.DukePrimeDegree.twoBlockNeutral_inverse_blocks line 24
  3. def OAI.DukePrimeDegree.twoBlockUpperAction line 38
  4. lemma OAI.DukePrimeDegree.twoBlockUpper_injective line 42
  5. theorem OAI.DukePrimeDegree.twoBlockNeutral_conjugate_upper line 48
  6. theorem OAI.DukePrimeDegree.twoBlockNeutral_upper_reorder line 60
  7. theorem OAI.DukePrimeDegree.twoBlockUpperAction_inv_apply line 66
  8. theorem OAI.DukePrimeDegree.twoBlockUpperAction_apply_inv line 74
  9. theorem OAI.DukePrimeDegree.twoBlockUpperAction_mul line 79
  10. theorem OAI.DukePrimeDegree.continuous_twoBlockUpperAction line 89
  11. theorem OAI.DukePrimeDegree.continuous_twoBlockUpperAction_inv line 104