OAI/GroupTheory/SimpleAmenable/RandomFields/PrimitiveCovariance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.spatialTranslate_zero line 14
  2. theorem OAI.SimpleAmenable.spatialTranslate_add line 20
  3. theorem OAI.SimpleAmenable.spatialTranslate_whole line 27
  4. def OAI.SimpleAmenable.CommonFrame.mul line 37
  5. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy_frame line 51
  6. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy_translate_eq line 57
  7. theorem OAI.SimpleAmenable.InitialCoverSystem.translatedAlphabet_mul line 64
  8. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy_conjugate line 74
  9. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveCopy_zero line 82
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.initialAlphabet_conjugate_common line 95
  11. theorem OAI.SimpleAmenable.copyFamilyEval_comp line 113
  12. theorem OAI.SimpleAmenable.copyFamilyEval_reindex_range line 119
  13. theorem OAI.SimpleAmenable.InitialCoverSystem.primitiveFamily_conjugate line 131
  14. theorem OAI.SimpleAmenable.InitialCoverSystem.PrimitiveFamilyLaw.translate line 141
  15. theorem OAI.SimpleAmenable.InitialCoverSystem.PrimitiveFamilyLaw.reindex line 150
  16. theorem OAI.SimpleAmenable.InitialCoverSystem.PrimitiveFamilyLaw.congr_offsets line 162