OAI/Combinatorics/Progressions/Geometry/NativeTernaryCoordinate.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BinaryTensorIndex line 11
  2. instance OAI.Erdos3.BinaryTensorIndex.fintype line 15
  3. def OAI.Erdos3.coordinateTranslatedInput line 24
  4. def OAI.Erdos3.coordinateTranslationHom line 27
  5. def OAI.Erdos3.coordinateReplaceIndex line 39
  6. def OAI.Erdos3.coordinateReplaceInput line 42
  7. theorem OAI.Erdos3.coordinateTranslation_sum line 45
  8. theorem OAI.Erdos3.coordinateTranslation_left line 54
  9. theorem OAI.Erdos3.coordinateTranslation_right line 58
  10. def OAI.Erdos3.coordinateTranslationExpansion line 69
  11. theorem OAI.Erdos3.coordinateTranslationExpansion_unit line 75
  12. def OAI.Erdos3.TernaryTensorIndex line 96
  13. instance OAI.Erdos3.TernaryTensorIndex.fintype line 100
  14. def OAI.Erdos3.ternaryCoordinateInput line 110
  15. def OAI.Erdos3.ternaryCoordinateHom line 113
  16. def OAI.Erdos3.ternaryReplaceIndex line 120
  17. def OAI.Erdos3.ternaryReplaceInput line 123
  18. theorem OAI.Erdos3.ternaryCoordinateInput_replace line 126
  19. theorem OAI.Erdos3.ternaryCoordinateInput_cons line 136
  20. def OAI.Erdos3.ternaryCoordinateExpansion line 146
  21. theorem OAI.Erdos3.ternaryCoordinateExpansion_unit line 153
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_coordinate_translation_equivalence line 174
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_ternary_coordinate_equivalence line 200