OAI/RepresentationTheory/UniversalSquare/Finite/SmallContracts13_1.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Small Contracts 13 1.

  1. def OAI.UniversalTensorSquare.smallB13_4 line 15
  2. def OAI.UniversalTensorSquare.smallT13_4 line 16
  3. def OAI.UniversalTensorSquare.smallFlag13_4 line 17
  4. lemma OAI.UniversalTensorSquare.smallCert13_4 line 18
  5. lemma OAI.UniversalTensorSquare.smallSupport13_4 line 22
  6. def OAI.UniversalTensorSquare.smallB13_5 line 31
  7. def OAI.UniversalTensorSquare.smallT13_5 line 32
  8. def OAI.UniversalTensorSquare.smallFlag13_5 line 33
  9. lemma OAI.UniversalTensorSquare.smallCert13_5 line 34
  10. lemma OAI.UniversalTensorSquare.smallSupport13_5 line 38
  11. def OAI.UniversalTensorSquare.smallB13_6 line 47
  12. def OAI.UniversalTensorSquare.smallT13_6 line 48
  13. def OAI.UniversalTensorSquare.smallFlag13_6 line 49
  14. lemma OAI.UniversalTensorSquare.smallCert13_6 line 50
  15. lemma OAI.UniversalTensorSquare.smallSupport13_6 line 54
  16. def OAI.UniversalTensorSquare.smallB13_7 line 63
  17. def OAI.UniversalTensorSquare.smallT13_7 line 64
  18. def OAI.UniversalTensorSquare.smallFlag13_7 line 65
  19. lemma OAI.UniversalTensorSquare.smallCert13_7 line 66
  20. lemma OAI.UniversalTensorSquare.smallSupport13_7 line 70