OAI/Combinatorics/Progressions/Geometry/RealifiedTripleCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.tripleNeutral line 12
  2. def OAI.Erdos3.tripleLeft line 17
  3. def OAI.Erdos3.tripleRight line 22
  4. def OAI.Erdos3.tripleAssemble line 27
  5. theorem OAI.Erdos3.tripleNeutral_assemble line 29
  6. theorem OAI.Erdos3.tripleLeft_assemble line 33
  7. theorem OAI.Erdos3.tripleRight_assemble line 37
  8. theorem OAI.Erdos3.tripleAssemble_decompose line 41
  9. theorem OAI.Erdos3.tripleAssemble_lie line 53
  10. def OAI.Erdos3.realTripleEquiv line 83
  11. theorem OAI.Erdos3.realTripleEquiv_tmul line 88
  12. theorem OAI.Erdos3.realTripleEquiv_neutral line 91
  13. theorem OAI.Erdos3.realTripleEquiv_left line 102
  14. theorem OAI.Erdos3.realTripleEquiv_right line 112
  15. theorem OAI.Erdos3.realTripleEquiv_first line 122
  16. theorem OAI.Erdos3.realTripleEquiv_second line 128
  17. theorem OAI.Erdos3.realTripleEquiv_third line 135