OAI/RepresentationTheory/UniversalSquare/Finite/SmallContracts13_9.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Small Contracts 13 9.

  1. def OAI.UniversalTensorSquare.smallB13_36 line 15
  2. def OAI.UniversalTensorSquare.smallT13_36 line 16
  3. def OAI.UniversalTensorSquare.smallFlag13_36 line 17
  4. lemma OAI.UniversalTensorSquare.smallCert13_36 line 18
  5. lemma OAI.UniversalTensorSquare.smallSupport13_36 line 22
  6. def OAI.UniversalTensorSquare.smallB13_37 line 31
  7. def OAI.UniversalTensorSquare.smallT13_37 line 32
  8. def OAI.UniversalTensorSquare.smallFlag13_37 line 33
  9. lemma OAI.UniversalTensorSquare.smallCert13_37 line 34
  10. lemma OAI.UniversalTensorSquare.smallSupport13_37 line 38
  11. def OAI.UniversalTensorSquare.smallB13_38 line 47
  12. def OAI.UniversalTensorSquare.smallT13_38 line 48
  13. def OAI.UniversalTensorSquare.smallFlag13_38 line 49
  14. lemma OAI.UniversalTensorSquare.smallCert13_38 line 50
  15. lemma OAI.UniversalTensorSquare.smallSupport13_38 line 54
  16. def OAI.UniversalTensorSquare.smallB13_39 line 63
  17. def OAI.UniversalTensorSquare.smallT13_39 line 64
  18. def OAI.UniversalTensorSquare.smallFlag13_39 line 65
  19. lemma OAI.UniversalTensorSquare.smallCert13_39 line 66
  20. lemma OAI.UniversalTensorSquare.smallSupport13_39 line 70