OAI/Computability/DepthThree/AlgebraQuotient.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.BinaryAlgebra.quotientRepresentative line 13
  2. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.quotientRepresentative_mk line 17
  3. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.mk_quotientRepresentative line 22
  4. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degree_quotientRepresentative_lt line 27
  5. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.quotientRepresentative_one line 35
  6. abbrev OAI.DepthThreeLowerBound.BinaryAlgebra.InputQuotient line 47
  7. abbrev OAI.DepthThreeLowerBound.BinaryAlgebra.BitQuotient line 50
  8. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.pack_mod_inputPolynomial line 53
  9. def OAI.DepthThreeLowerBound.BinaryAlgebra.encode line 59
  10. def OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates line 62
  11. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates_apply line 88
  12. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates_symm_apply line 93
  13. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates_encode line 96
  14. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.encode_coordinates line 100
  15. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.encode_injective line 104
  16. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.encode_surjective line 107
  17. instance OAI.DepthThreeLowerBound.BinaryAlgebra.inputQuotientFintype line 110
  18. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.inputQuotient_card line 113
  19. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitQuotient_card line 118
  20. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates_mk line 122
  21. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.encode_zero line 128
  22. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.encode_add line 132
  23. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.encode_smul line 136
  24. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates_encode_mul line 142
  25. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.encode_mul line 150
  26. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates_mul line 158
  27. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.coordinates_one line 164
  28. def OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero line 169
  29. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero_apply line 172
  30. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero_mk line 176
  31. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero_one line 180
  32. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero_surjective line 184
  33. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero_encode line 190
  34. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero_coordinates line 195
  35. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.degreeZero_sum_encode_pow line 199