OAI/NumberTheory/OrdinaryCorrelations/HighTrace/SupportIffExtraOrLabel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.support_iff_extra_or_label line 20
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.activity line 32
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.activity_divides line 37
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.tail_support line 48
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.occurs_before_or_tail line 52
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.free_prime_one_side line 71
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.attached_activity_comparison line 85