OAI/Analysis/FreeGroupFactor/Generation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Generation.mapTuple line 17
  2. theorem OAI.FreeGroupFactorMain.Generation.mapTuple_coe line 20
  3. theorem OAI.FreeGroupFactorMain.Generation.word_mapTuple line 23
  4. theorem OAI.FreeGroupFactorMain.Generation.poly_mapTuple line 31
  5. def OAI.FreeGroupFactorMain.Generation.substitute line 36
  6. def OAI.FreeGroupFactorMain.Generation.wordTuple line 39
  7. theorem OAI.FreeGroupFactorMain.Generation.word_wordTuple line 42
  8. theorem OAI.FreeGroupFactorMain.Generation.poly_substitute line 51
  9. instance OAI.FreeGroupFactorMain.Generation.unitary_isClosed line 59
  10. instance OAI.FreeGroupFactorMain.Generation.unitary_completeSpace line 62
  11. theorem OAI.FreeGroupFactorMain.Generation.word_canonical line 68
  12. theorem OAI.FreeGroupFactorMain.Generation.canonical_poly_dense line 78
  13. theorem OAI.FreeGroupFactorMain.Generation.automorphism_poly_dense line 100
  14. abbrev OAI.FreeGroupFactorMain.Generation.Ambient line 112
  15. abbrev OAI.FreeGroupFactorMain.Generation.Tuple line 113
  16. def OAI.FreeGroupFactorMain.Generation.initial line 114
  17. theorem OAI.FreeGroupFactorMain.Generation.word_initial line 116
  18. def OAI.FreeGroupFactorMain.Generation.orbit line 127
  19. theorem OAI.FreeGroupFactorMain.Generation.orbit_nonempty line 131
  20. theorem OAI.FreeGroupFactorMain.Generation.mapTuple_trans line 136
  21. theorem OAI.FreeGroupFactorMain.Generation.orbit_step line 140
  22. theorem OAI.FreeGroupFactorMain.Generation.poly_groupL2_continuous line 174
  23. theorem OAI.FreeGroupFactorMain.Generation.orbit_local_approximation line 178
  24. theorem OAI.FreeGroupFactorMain.Generation.orbit_trace line 205
  25. theorem OAI.FreeGroupFactorMain.Generation.closure_orbit_trace line 215
  26. theorem OAI.FreeGroupFactorMain.Generation.poly_l2_mem line 224
  27. theorem OAI.FreeGroupFactorMain.Generation.total_of_poly_approx line 234
  28. theorem OAI.FreeGroupFactorMain.baire_local_approximation line 252
  29. theorem OAI.FreeGroupFactorMain.normalTracialIso_of_groupEquiv line 289
  30. theorem OAI.FreeGroupFactorMain.HasNormalTracialIso.trans line 310
  31. def OAI.FreeGroupFactorMain.optionRankEquiv line 322
  32. theorem OAI.FreeGroupFactorMain.generating_haar_tuple line 327
  33. theorem OAI.FreeGroupFactorMain.rank_step_option line 338
  34. theorem OAI.FreeGroupFactorMain.rank_step line 348