OAI/Computability/WLIdentification/RingPresentation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.FinitePresentation.vectorTwo line 10
  2. structure OAI.WLIdentification.FinitePresentation.RingRealizer line 12
  3. abbrev OAI.WLIdentification.FinitePresentation.RingRealizer.rowP line 36
  4. abbrev OAI.WLIdentification.FinitePresentation.RingRealizer.hBase line 37
  5. abbrev OAI.WLIdentification.FinitePresentation.RingRealizer.vBase line 38
  6. abbrev OAI.WLIdentification.FinitePresentation.RingRealizer.sBase line 39
  7. def OAI.WLIdentification.FinitePresentation.RingRealizer.nextRow line 41
  8. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.nextRow_eq line 43
  9. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.nextRow_poly line 46
  10. def OAI.WLIdentification.FinitePresentation.RingRealizer.hAllowed line 51
  11. def OAI.WLIdentification.FinitePresentation.RingRealizer.sAllowed line 54
  12. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.hBase_code line 57
  13. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.sBase_code line 59
  14. def OAI.WLIdentification.FinitePresentation.RingRealizer.labelsPair line 62
  15. def OAI.WLIdentification.FinitePresentation.RingRealizer.hEquiv line 81
  16. def OAI.WLIdentification.FinitePresentation.RingRealizer.hP line 87
  17. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.hP_code line 90
  18. def OAI.WLIdentification.FinitePresentation.RingRealizer.matchingPair line 93
  19. def OAI.WLIdentification.FinitePresentation.RingRealizer.sEquiv line 112
  20. def OAI.WLIdentification.FinitePresentation.RingRealizer.sP line 118
  21. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.sP_code line 121
  22. def OAI.WLIdentification.FinitePresentation.RingRealizer.vEquiv line 124
  23. def OAI.WLIdentification.FinitePresentation.RingRealizer.vP line 130
  24. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.vP_code line 133
  25. def OAI.WLIdentification.FinitePresentation.RingRealizer.hDim line 136
  26. def OAI.WLIdentification.FinitePresentation.RingRealizer.cP line 141
  27. def OAI.WLIdentification.FinitePresentation.RingRealizer.bP line 142
  28. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.cP_inl line 144
  29. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.cP_inr line 146
  30. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.bP_inl line 147
  31. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.bP_inr line 148