OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ActivityResidue.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.activity_residue line 18
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.attached_activity_comparison_residues line 27
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.holds_residues line 44
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sortPrivateFamily line 55
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.sortPrivateFamily_witness line 66