OAI/Analysis/InterpolatedFactors/Subalgebras.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.subalgebraEqualityEquiv line 14
  2. theorem OAI.FreeGroupFactorMain.Amplification.subalgebraEqualityEquiv_val line 17
  3. theorem OAI.FreeGroupFactorMain.Amplification.subtype_projection line 25
  4. def OAI.FreeGroupFactorMain.Amplification.cornerSubtypeEquiv line 28
  5. theorem OAI.FreeGroupFactorMain.Amplification.projectionRepresentation_normal line 40
  6. theorem OAI.FreeGroupFactorMain.Amplification.projectionRepresentation_symm_normal line 57
  7. def OAI.FreeGroupFactorMain.Amplification.subalgebraTopology line 78
  8. theorem OAI.FreeGroupFactorMain.Amplification.subalgebraEquiv_normal line 81
  9. theorem OAI.FreeGroupFactorMain.Amplification.subalgebraEquiv_symm_normal line 90
  10. theorem OAI.FreeGroupFactorMain.Amplification.subalgebraEqualityEquiv_normal line 99
  11. theorem OAI.FreeGroupFactorMain.Amplification.subalgebraEqualityEquiv_symm_normal line 103
  12. theorem OAI.FreeGroupFactorMain.Amplification.cornerCongr_symm_normal line 107
  13. theorem OAI.FreeGroupFactorMain.Amplification.cornerSubtypeEquiv_normal line 120
  14. theorem OAI.FreeGroupFactorMain.Amplification.cornerSubtypeEquiv_symm_normal line 130
  15. theorem OAI.FreeGroupFactorMain.FreeFock.gaussianGroupIso_symm_normal line 147
  16. instance OAI.FreeGroupFactorMain.FreeFock.scalarGeneratedClosed line 159
  17. def OAI.FreeGroupFactorMain.FreeFock.scalarGroupIso line 162
  18. theorem OAI.FreeGroupFactorMain.FreeFock.scalarGroupIso_normal line 165
  19. theorem OAI.FreeGroupFactorMain.FreeFock.scalarGroupIso_symm_normal line 174
  20. def OAI.FreeGroupFactorMain.FreeFock.scalarTrace line 185
  21. theorem OAI.FreeGroupFactorMain.FreeFock.scalarGroupIso_trace line 187
  22. theorem OAI.FreeGroupFactorMain.Amplification.nested_projection line 196
  23. theorem OAI.FreeGroupFactorMain.Amplification.nested_supported line 199
  24. def OAI.FreeGroupFactorMain.Amplification.nestedCornerEquiv line 208
  25. theorem OAI.FreeGroupFactorMain.Amplification.nestedCornerEquiv_normal line 219
  26. theorem OAI.FreeGroupFactorMain.Amplification.nestedCornerEquiv_symm_normal line 227
  27. def OAI.FreeGroupFactorMain.Amplification.HasCornerScaling line 238
  28. theorem OAI.FreeGroupFactorMain.Amplification.HasCornerScaling.mul line 245
  29. theorem OAI.FreeGroupFactorMain.Amplification.HasCornerScaling.normalized line 273