OAI/Combinatorics/Progressions/Geometry/SpatialPivotNormalization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.UnselectedColumn line 14
  2. instance OAI.Erdos3.unselectedColumnFintype line 16
  3. def OAI.Erdos3.selectedColumnEquiv line 19
  4. def OAI.Erdos3.selectedSpatialColumnEquiv line 24
  5. def OAI.Erdos3.selectedSpatialPivot line 29
  6. def OAI.Erdos3.selectedSpatialFreeColumns line 33
  7. theorem OAI.Erdos3.selectedSpatial_fromCols line 37
  8. theorem OAI.Erdos3.selectedSpatial_mulVec line 46
  9. def OAI.Erdos3.spatialPivotScale line 64
  10. theorem OAI.Erdos3.spatialPivotScale_pos line 67
  11. theorem OAI.Erdos3.normalized_selectedSpatialPivot line 74
  12. theorem OAI.Erdos3.rootDifferenceMatrix_real_bound line 100
  13. theorem OAI.Erdos3.normalizedPivotEquiv_inverse_eq line 112