OAI/Computability/DepthThree/AlgebraLanguage.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.ParsedInput.QuotientRing line 14
  2. instance OAI.DepthThreeLowerBound.ParsedInput.quotientRingFintype line 16
  3. def OAI.DepthThreeLowerBound.ParsedInput.quotientHash line 20
  4. def OAI.DepthThreeLowerBound.ParsedInput.quotientCoefficient line 23
  5. def OAI.DepthThreeLowerBound.ParsedInput.quotientEvaluation line 26
  6. theorem OAI.DepthThreeLowerBound.ParsedInput.quotientHash_eq_encode line 29
  7. theorem OAI.DepthThreeLowerBound.ParsedInput.quotientCoefficient_eq_encode line 34
  8. def OAI.DepthThreeLowerBound.ParsedInput.coefficientBitsEquiv line 39
  9. theorem OAI.DepthThreeLowerBound.ParsedInput.coefficientBitsEquiv_apply line 45
  10. theorem OAI.DepthThreeLowerBound.ParsedInput.coefficientBitsEquiv_coefficient line 51
  11. theorem OAI.DepthThreeLowerBound.ParsedInput.quotientRing_card line 55
  12. theorem OAI.DepthThreeLowerBound.ParsedInput.quotientEvaluation_eq_mk line 59
  13. theorem OAI.DepthThreeLowerBound.ParsedInput.representative_quotientEvaluation line 64
  14. theorem OAI.DepthThreeLowerBound.ParsedInput.degreeZero_quotientEvaluation line 70
  15. theorem OAI.DepthThreeLowerBound.ParsedInput.quotient_degreeZero_one line 75
  16. theorem OAI.DepthThreeLowerBound.ParsedInput.evaluate_eq_true_iff_degreeZero line 82
  17. theorem OAI.DepthThreeLowerBound.language_eq_true_iff_quotient line 89