OAI/Computability/WLIdentification/RingMembership.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.hCoord_iff line 13
  2. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.vCoord_iff line 25
  3. def OAI.WLIdentification.FinitePresentation.RingRealizer.memberEval line 29
  4. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.member_ee line 34
  5. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.member_eo line 36
  6. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.member_oe line 38
  7. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.member_oo line 41
  8. theorem OAI.WLIdentification.FinitePresentation.RingRealizer.memberEval_poly line 45
  9. def OAI.WLIdentification.FinitePresentation.RingRealizer.member line 65
  10. def OAI.WLIdentification.FinitePresentation.RingRealizer.localData line 100