OAI/RepresentationTheory/UniversalSquare/Support/CoordinateLine.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Coordinate Line.

  1. def OAI.Saxl.coordinateRestriction line 15
  2. def OAI.Saxl.projectedCoordinate line 21
  3. lemma OAI.Saxl.projectedCoordinate_pair line 25
  4. lemma OAI.Saxl.projectedCoordinate_nonzero line 31
  5. lemma OAI.Saxl.coordinateRestriction_nonzero line 41
  6. lemma OAI.Saxl.coordinateRestriction_fixed line 47
  7. lemma OAI.Saxl.projectedCoordinate_fixed line 58
  8. theorem OAI.Saxl.signEquiv_coordinate_line line 68
  9. lemma OAI.Saxl.exists_tableau_of_row_content line 102
  10. theorem OAI.Saxl.coordinateRestriction_ne_zero_of_content line 110