OAI/RepresentationTheory/UniversalSquare/Specht/ThreeRowTensors.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Three Row Tensors.

  1. def OAI.Saxl.ThreeRow.powerVector line 15
  2. lemma OAI.Saxl.ThreeRow.wordMap_constant line 18
  3. lemma OAI.Saxl.ThreeRow.powerVector_smul line 23
  4. def OAI.Saxl.ThreeRow.independentTensor line 28
  5. def OAI.Saxl.ThreeRow.symmetricIndex line 34
  6. def OAI.Saxl.ThreeRow.matrixCoord line 36
  7. def OAI.Saxl.ThreeRow.xCoord line 37
  8. def OAI.Saxl.ThreeRow.yCoord line 38
  9. def OAI.Saxl.ThreeRow.independentFamily line 40
  10. lemma OAI.Saxl.ThreeRow.gram_symm line 45
  11. lemma OAI.Saxl.ThreeRow.matrixCoord_parameter line 49
  12. lemma OAI.Saxl.ThreeRow.xCoord_parameter line 55
  13. lemma OAI.Saxl.ThreeRow.yCoord_parameter line 59
  14. lemma OAI.Saxl.ThreeRow.independentFamily_analytic line 63
  15. def OAI.Saxl.ThreeRow.packCoordinates line 84
  16. lemma OAI.Saxl.ThreeRow.matrixCoord_pack line 87
  17. lemma OAI.Saxl.ThreeRow.xCoord_pack line 93
  18. lemma OAI.Saxl.ThreeRow.yCoord_pack line 98
  19. lemma OAI.Saxl.ThreeRow.independentFamily_pack line 103
  20. lemma OAI.Saxl.ThreeRow.wordMap_symmetricPairs line 109
  21. lemma OAI.Saxl.ThreeRow.colorTensor_image line 117
  22. theorem OAI.Saxl.ThreeRow.independent_nonvanishing line 127