OAI/NumberTheory/OrdinaryCorrelations/HighTrace/OrientedSubpathRefl.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.orientedSubpath_refl line 18
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.orientedSubpath_trans line 23
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.qualifies_transfer line 72
4. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.primitive_descent line 86
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.orientedSubpath_start line 105