OAI/Combinatorics/SumProduct/Alignment/CentralQuotient01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompactGroupProducts.HasCompactReps line 17
  2. lemma OAI.CompactGroupProducts.isClosed_subset_lattice line 24
  3. lemma OAI.CompactGroupProducts.HasCompactReps.isClosed line 36
  4. theorem OAI.CompactGroupProducts.HasCompactReps.discrete_map line 54
  5. lemma OAI.CompactGroupProducts.HasCompactReps.quotient_compactSpace line 108
  6. lemma OAI.CompactGroupProducts.HasCompactReps.map_surjective line 122
  7. theorem OAI.CompactGroupProducts.rational_normal_quotient line 135
  8. lemma OAI.CentralQuotientAction.central_kernel_normal line 153
  9. lemma OAI.CentralQuotientAction.central_action_kernel line 161
  10. def OAI.CentralQuotientAction.action line 172
  11. theorem OAI.CentralQuotientAction.action_mk line 177
  12. lemma OAI.CentralQuotientAction.continuous_action line 184
  13. lemma OAI.CentralQuotientAction.compact_central_quotient line 196
  14. theorem OAI.CentralQuotientAction.quotientMap_fibers line 216
  15. lemma OAI.CentralQuotientAction.invariant_central_action line 249
  16. lemma OAI.CentralQuotientAction.quotientMap_smul line 261
  17. lemma OAI.CentralQuotientAction.invariant_quotientMap line 269