OAI/Analysis/FreeGroupFactor/Nielsen.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.groupL2_groupUnitary line 17
  2. theorem OAI.FreeGroupFactorMain.group_single_total line 25
  3. theorem OAI.FreeGroupFactorMain.spatialGroupIso_symm_normal line 41
  4. def OAI.FreeGroupFactorMain.gaugedRepresentation line 56
  5. theorem OAI.FreeGroupFactorMain.gaugedRepresentation_apply line 66
  6. theorem OAI.FreeGroupFactorMain.gaugedRepresentation_star line 69
  7. theorem OAI.FreeGroupFactorMain.gaugedRepresentation_trace line 77
  8. theorem OAI.FreeGroupFactorMain.gaugedRepresentation_total line 89
  9. theorem OAI.FreeGroupFactorMain.gaugedIso line 104
  10. def OAI.FreeGroupFactorMain.nielsenHom line 129
  11. theorem OAI.FreeGroupFactorMain.nielsenHom_of_some line 133
  12. theorem OAI.FreeGroupFactorMain.nielsenHom_of_none line 137
  13. theorem OAI.FreeGroupFactorMain.nielsenHom_map_some line 141
  14. theorem OAI.FreeGroupFactorMain.nielsenHom_inv_comp line 149
  15. def OAI.FreeGroupFactorMain.nielsenEquiv line 155
  16. theorem OAI.FreeGroupFactorMain.gauged_nielsen_iso line 162