OAI/Computability/PerfectCompleteness/Repetition/CleanTreeFactors.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanTreeFactors.Index line 21
  2. def OAI.PerfectCompleteness.CleanTreeFactors.height line 24
  3. def OAI.PerfectCompleteness.CleanTreeFactors.square line 28
  4. def OAI.PerfectCompleteness.CleanTreeFactors.factorIds line 32
  5. abbrev OAI.PerfectCompleteness.CleanTreeFactors.Factors line 38
  6. abbrev OAI.PerfectCompleteness.CleanTreeFactors.Raw line 42
  7. instance OAI.PerfectCompleteness.CleanTreeFactors.rawFintype line 46
  8. def OAI.PerfectCompleteness.CleanTreeFactors.zeroRaw line 50
  9. instance OAI.PerfectCompleteness.CleanTreeFactors.rawNonempty line 54
  10. def OAI.PerfectCompleteness.CleanTreeFactors.rawEquiv line 58
  11. theorem OAI.PerfectCompleteness.CleanTreeFactors.rawEquiv_zero line 72
  12. def OAI.PerfectCompleteness.CleanTreeFactors.rawLaw line 78
  13. theorem OAI.PerfectCompleteness.CleanTreeFactors.rawLaw_uniform line 83
  14. def OAI.PerfectCompleteness.CleanTreeFactors.allZero line 94
  15. theorem OAI.PerfectCompleteness.CleanTreeFactors.allZero_rawEquiv line 99
  16. theorem OAI.PerfectCompleteness.CleanTreeFactors.probability_allZero line 116
  17. theorem OAI.PerfectCompleteness.CleanTreeFactors.probability_allZero_pos line 130