OAI/NumberTheory/DukePrimeDegree/Dynamics/SingularCentralizer.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual centralizer of a singular diagonal

Equal weights determine the neutral blocks. The resulting concrete block matrix subgroup is precisely the centralizer of any nonzero time of the diagonal flow. No symmetry assertion about the measure's invariant-root relation is used in this identification.

  1. def OAI.DukePrimeDegree.weightBlockSetoid line 21
  2. lemma OAI.DukePrimeDegree.matrix_commute_weight_diagonal_iff line 25
  3. theorem OAI.DukePrimeDegree.mem_weightBlockGroup_iff_commute_flow line 50