OAI/Computability/WLIdentification/RingLegality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.FinitePresentation.RingRealizer.readH line 13
  2. def OAI.WLIdentification.FinitePresentation.RingRealizer.readV line 14
  3. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.readH_cast line 16
  4. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.leftVector line 19
  5. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.rightVector line 34
  6. def OAI.WLIdentification.FinitePresentation.RingRealizer.firstTerm line 49
  7. def OAI.WLIdentification.FinitePresentation.RingRealizer.secondTerm line 51
  8. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.firstTerm_eq line 54
  9. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.secondTerm_eq line 69
  10. def OAI.WLIdentification.FinitePresentation.RingRealizer.formEval line 84
  11. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.formEval_eq line 88
  12. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.readH_poly line 100
  13. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.readV_poly line 104
  14. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.firstTerm_poly line 109
  15. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.secondTerm_poly line 114
  16. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.formEval_poly line 120
  17. def OAI.WLIdentification.FinitePresentation.RingRealizer.legal line 137
  18. def OAI.WLIdentification.FinitePresentation.RingRealizer.affine line 168