OAI/RepresentationTheory/UniversalSquare/Band/OddPath.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Odd Path.

  1. def OAI.Saxl.Band.basisCoordinates line 13
  2. def OAI.Saxl.Band.matrixBasisEquiv line 23
  3. def OAI.Saxl.Band.conjugationEquiv line 37
  4. def OAI.Saxl.Band.pathBasis line 49
  5. lemma OAI.Saxl.Band.pathBasis_apply line 52
  6. def OAI.Saxl.Columns.dualBlockWord line 60
  7. lemma OAI.Saxl.Columns.chainFunctional_dualBlockWord line 64
  8. theorem OAI.Saxl.Columns.odd_path_ordered_contraction line 70