OAI/NumberTheory/OrdinaryCorrelations/HighTrace/PrivateFamily.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily line 19
  2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.key_injective line 30
  3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Intrinsic line 35
  4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.PreTail line 41
  5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.FirstTail line 45
  6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.LastTail line 48
  7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.BeforeLine line 51
  8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.AfterLine line 54
  9. inductive OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Case line 57
  10. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.(instance at line 61) line 61
  11. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.(instance at line 64) line 64
  12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.case_card line 66
  13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.CaseHolds line 68
  14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.exists_case line 78
  15. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.large_case line 104
  16. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.exists_tails line 117