OAI/RepresentationTheory/UniversalSquare/Specht/ColumnTensorSplit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Column Tensor Split.

  1. def OAI.Saxl.FlagColumns.splitCons line 15
  2. lemma OAI.Saxl.FlagColumns.splitCons_left_first line 21
  3. lemma OAI.Saxl.FlagColumns.splitCons_right_first line 26
  4. lemma OAI.Saxl.FlagColumns.splitCons_left_rest line 31
  5. lemma OAI.Saxl.FlagColumns.splitCons_right_rest line 36
  6. def OAI.Saxl.FlagColumns.splitPositions line 41
  7. lemma OAI.Saxl.FlagColumns.splitPositions_left_first line 47
  8. lemma OAI.Saxl.FlagColumns.splitPositions_right_first line 52
  9. lemma OAI.Saxl.FlagColumns.splitPositions_left_rest line 57
  10. lemma OAI.Saxl.FlagColumns.splitPositions_right_rest line 63
  11. theorem OAI.Saxl.FlagColumns.tensorList_split line 69
  12. lemma OAI.Saxl.FlagColumns.blocks_eq_tensorList line 115