OAI/Computability/PerfectCompleteness/Construction/OriginalChildScalars.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalChildScalars.product_swap line 18
  2. theorem OAI.PerfectCompleteness.OriginalChildScalars.product_swap_map line 27
  3. abbrev OAI.PerfectCompleteness.OriginalChildScalars.Square line 40
  4. instance OAI.PerfectCompleteness.OriginalChildScalars.squareFintype line 43
  5. def OAI.PerfectCompleteness.OriginalChildScalars.squareSum line 46
  6. def OAI.PerfectCompleteness.OriginalChildScalars.specialSquareLaw line 54
  7. def OAI.PerfectCompleteness.OriginalChildScalars.squareComponent line 60
  8. theorem OAI.PerfectCompleteness.OriginalChildScalars.squareComponent_self line 65
  9. theorem OAI.PerfectCompleteness.OriginalChildScalars.squareComponent_other line 70
  10. abbrev OAI.PerfectCompleteness.OriginalChildScalars.ScalarTape line 76
  11. def OAI.PerfectCompleteness.OriginalChildScalars.selectedAndOthers line 80
  12. def OAI.PerfectCompleteness.OriginalChildScalars.stepSquareMap line 87
  13. theorem OAI.PerfectCompleteness.OriginalChildScalars.selectedAndOthers_law line 93
  14. theorem OAI.PerfectCompleteness.OriginalChildScalars.squareComponent_otherLaw line 110
  15. theorem OAI.PerfectCompleteness.OriginalChildScalars.stepSquareMap_law line 119
  16. def OAI.PerfectCompleteness.OriginalChildScalars.callsLaw line 158
  17. def OAI.PerfectCompleteness.OriginalChildScalars.callContributions line 164
  18. def OAI.PerfectCompleteness.OriginalChildScalars.callComponent line 170
  19. theorem OAI.PerfectCompleteness.OriginalChildScalars.callContributions_law line 175