OAI/Geometry/NilpotentCharts/CompactGroups.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Compact-power rigidity, centralizers and uniqueness of one-parameter subgroups.

  1. def OAI.RawCompactNilpotent.NoCompactPowers line 13
  2. def OAI.RawCompactNilpotent.CompactConjugacyCentral line 16
  3. lemma OAI.RawCompactNilpotent.eq_zero_of_compact_nsmul line 19
  4. lemma OAI.RawCompactNilpotent.noCompactPowers_extension line 34
  5. lemma OAI.RawCompactNilpotent.conjugate_pow_of_central_commutator line 44
  6. lemma OAI.RawCompactNilpotent.compactConjugacy_extension line 66
  7. theorem OAI.RawCompactNilpotent.centralizer_cocompact_le_center line 98
  8. lemma OAI.RawCompactNilpotent.noCompactPowers_vector_subgroup line 125
  9. lemma OAI.RawPowerExtension.pow_injective_extension line 156
  10. lemma OAI.RawPowerExtension.no_torsion_of_no_compact_powers line 174
  11. lemma OAI.RawPowerExtension.real_oneparameter_unique line 186