OAI/RepresentationTheory/UniversalSquare/Contraction/TwoPathContraction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Two Path Contraction.

  1. lemma OAI.Saxl.Columns.dualBlockWord_singleton line 14
  2. lemma OAI.Saxl.Columns.dotProduct_cast line 30
  3. lemma OAI.Saxl.Columns.columnWedge_path_nonzero line 37
  4. theorem OAI.Saxl.Columns.two_path_contraction line 48
  5. theorem OAI.Saxl.Columns.two_path_cyclic_support line 61
  6. lemma OAI.Saxl.Columns.positionProduct_move line 80
  7. theorem OAI.Saxl.Columns.two_path_cyclic_support_placed line 92
  8. theorem OAI.Saxl.Columns.odd_column_split line 117