OAI/NumberTheory/OrdinaryCorrelations/HighTrace/CoefficientZeroOfNotSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.coefficient_zero_of_not_support line 20
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.before_segment_absent line 33
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.after_segment_absent line 44
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.comparisonSupport line 55
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.future_absent_before line 59
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.future_absent_after line 66
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.own_segment_absent_before line 73
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.own_segment_absent_after line 77