OAI/RepresentationTheory/UniversalSquare/Contraction/SingletonForms.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Singleton Forms.

  1. def OAI.Saxl.singleWord line 15
  2. lemma OAI.Saxl.wordMap_singleWord line 17
  3. def OAI.Saxl.pairSingletonTensor line 27
  4. lemma OAI.Saxl.wordMap_pairSingletonTensor line 31
  5. def OAI.Saxl.pairSingletonEquiv line 41
  6. lemma OAI.Saxl.pairSingletonEquiv_left line 48
  7. lemma OAI.Saxl.pairSingletonEquiv_right line 55
  8. lemma OAI.Saxl.pairSingletonEquiv_last line 61
  9. lemma OAI.Saxl.pairSingletonTensor_one line 68
  10. lemma OAI.Saxl.pairSingletonTensor_smul line 102
  11. theorem OAI.Saxl.one_odd_row_pairSingleton_support line 112
  12. lemma OAI.Saxl.shortPair_singleton_nonzero line 137
  13. theorem OAI.Saxl.one_odd_row_shortPair_support line 143