OAI/RepresentationTheory/UniversalSquare/Contraction/PairForms.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Pair Forms.

  1. def OAI.Saxl.pairFormTensor line 15
  2. lemma OAI.Saxl.pairFormTensor_one line 19
  3. lemma OAI.Saxl.pairFormTensor_smul line 32
  4. def OAI.Saxl.pairWordsEquiv line 38
  5. lemma OAI.Saxl.pairWordsEquiv_apply line 43
  6. lemma OAI.Saxl.wordMap_pairFormTensor line 47
  7. theorem OAI.Saxl.even_rows_pairFormTensor_support line 80
  8. def OAI.Saxl.shortPairForm line 99
  9. def OAI.Saxl.shortPairCongruence line 102
  10. lemma OAI.Saxl.shortPairCongruence_gram line 105
  11. theorem OAI.Saxl.even_rows_shortPair_support line 114
  12. def OAI.Saxl.outputTwoForm line 122
  13. def OAI.Saxl.outputTwoCongruence line 124
  14. lemma OAI.Saxl.outputTwoCongruence_gram line 126
  15. theorem OAI.Saxl.even_rows_outputTwo_support line 135