OAI/RepresentationTheory/UniversalSquare/Support/SquareSemigroup.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Square Semigroup.

  1. def OAI.UniversalTensorSquare.signTensorCancel line 16
  2. def OAI.UniversalTensorSquare.tensorRepEquiv line 27
  3. lemma OAI.UniversalTensorSquare.kronecker_pos_of_shapes line 36
  4. lemma OAI.UniversalTensorSquare.kronecker_pos_input_transpose line 58
  5. def OAI.UniversalTensorSquare.SquareOccurs line 80
  6. lemma OAI.UniversalTensorSquare.SquareOccurs.card_eq line 83
  7. lemma OAI.UniversalTensorSquare.SquareOccurs.pos line 88
  8. lemma OAI.UniversalTensorSquare.SquareOccurs.input_transpose line 95
  9. lemma OAI.UniversalTensorSquare.SquareOccurs.target_transpose line 100
  10. lemma OAI.UniversalTensorSquare.columnShape_perm line 108
  11. lemma OAI.UniversalTensorSquare.SquareOccurs.append line 115
  12. lemma OAI.UniversalTensorSquare.columnShape_diagram line 129
  13. lemma OAI.UniversalTensorSquare.columnShape_sorted line 138