OAI/NumberTheory/OrdinaryCorrelations/HighTrace/GlobalRecord.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord line 19
  2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.line_eq_of_labels_signs line 31
  3. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.RawCode line 44
  4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.rawCode line 48
  5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.rawCode_injective line 52
  6. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.(instance at line 78) line 78
  7. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.(instance at line 79) line 79
  8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.majorantSum line 81
  9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.Fiber line 84
  10. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.(instance at line 88) line 88
  11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.toPacket line 91
  12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.toPacket_injective line 99
  13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GlobalRecord.fiber_sum_le line 108