OAI/Computability/WLIdentification/RingCodes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.firstLabel_poly_of line 13
  2. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.secondLabel_poly_of line 21
  3. def OAI.WLIdentification.FinitePresentation.RingRealizer.leftCode line 29
  4. def OAI.WLIdentification.FinitePresentation.RingRealizer.rightCode line 34
  5. def OAI.WLIdentification.FinitePresentation.RingRealizer.topCode line 39
  6. def OAI.WLIdentification.FinitePresentation.RingRealizer.bottomCode line 41
  7. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.leftCode_eq line 44
  8. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.rightCode_eq line 49
  9. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.topCode_eq line 54
  10. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.bottomCode_eq line 58
  11. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.leftCode_poly line 62
  12. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.rightCode_poly line 73
  13. def OAI.WLIdentification.FinitePresentation.RingRealizer.hIndex line 85
  14. def OAI.WLIdentification.FinitePresentation.RingRealizer.vIndex line 89
  15. def OAI.WLIdentification.FinitePresentation.RingRealizer.sIndex line 93
  16. def OAI.WLIdentification.FinitePresentation.RingRealizer.hcIndex line 98
  17. def OAI.WLIdentification.FinitePresentation.RingRealizer.colors line 106