OAI/GroupTheory/SimpleAmenable/Arithmetic/PolygonArithmetic.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.CutRing line 14
  2. def OAI.SimpleAmenable.ordinary line 16
  3. def OAI.SimpleAmenable.conjugate line 21
  4. theorem OAI.SimpleAmenable.ordinary_apply line 26
  5. theorem OAI.SimpleAmenable.conjugate_apply line 30
  6. theorem OAI.SimpleAmenable.golden_coefficients_unique line 34
  7. theorem OAI.SimpleAmenable.ordinary_injective line 42
  8. theorem OAI.SimpleAmenable.conjugate_eq_ordinary_star line 50
  9. theorem OAI.SimpleAmenable.conjugate_injective line 56
  10. theorem OAI.SimpleAmenable.cut_norm_identity line 61
  11. theorem OAI.SimpleAmenable.cut_norm_nonzero line 67
  12. theorem OAI.SimpleAmenable.one_le_abs_cut_norm line 73
  13. def OAI.SimpleAmenable.endpointLabel line 78
  14. theorem OAI.SimpleAmenable.endpointLabel_embedding line 80
  15. abbrev OAI.SimpleAmenable.cutTau line 88
  16. theorem OAI.SimpleAmenable.ordinary_cutTau line 90
  17. theorem OAI.SimpleAmenable.conjugate_cutTau line 91
  18. theorem OAI.SimpleAmenable.cutTau_isUnit line 93
  19. def OAI.SimpleAmenable.cutForm line 97
  20. def OAI.SimpleAmenable.integralCutForm line 101
  21. theorem OAI.SimpleAmenable.cutForm_ordinary line 104
  22. theorem OAI.SimpleAmenable.cutForm_add line 108
  23. def OAI.SimpleAmenable.AvoidsCuts line 112
  24. theorem OAI.SimpleAmenable.avoidsCuts_translate line 115
  25. def OAI.SimpleAmenable.GenericSquare line 122
  26. def OAI.SimpleAmenable.halfPlane line 125
  27. def OAI.SimpleAmenable.polygonAlgebra line 128
  28. theorem OAI.SimpleAmenable.polygon_induction line 131