OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Test.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test line 23
  2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.selected line 32
  3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.modulus line 37
  4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.support line 42
  5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.expression line 47
  6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.coefficient line 56
  7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.Valid line 65
  8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.Linear line 79
  9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.selected_mem line 84
  10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.comparison_coefficient line 95
  11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.holds line 107
  12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.nondegenerate line 116
  13. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.modulus_ne_selected line 139