OAI/Computability/DepthThree/AlgebraBits.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.BinaryAlgebra.F2 line 11
  2. def OAI.DepthThreeLowerBound.BinaryAlgebra.boolEquivF2 line 13
  3. def OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue line 15
  4. def OAI.DepthThreeLowerBound.BinaryAlgebra.fieldBit line 17
  5. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_false line 19
  6. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_true line 21
  7. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.fieldBit_zero line 23
  8. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.fieldBit_one line 25
  9. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.fieldBit_bitValue line 27
  10. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_fieldBit line 30
  11. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_injective line 33
  12. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_surjective line 36
  13. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_xor line 39
  14. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_and line 43
  15. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_not line 47
  16. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_eq_zero_iff line 50
  17. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitValue_eq_one_iff line 53
  18. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.eq_zero_or_one line 56
  19. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.fieldBit_eq_false_iff line 60
  20. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.fieldBit_eq_true_iff line 64
  21. def OAI.DepthThreeLowerBound.BinaryAlgebra.bitsEquivF2 line 68
  22. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitsEquivF2_apply line 74
  23. theorem OAI.DepthThreeLowerBound.BinaryAlgebra.bitsEquivF2_symm_apply line 77