OAI/NumberTheory/OrdinaryCorrelations/HighTrace/GapPathCode.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapPathCodeline 25 - def
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PatternExpression.gapline 29 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PatternExpression.gap_relabelline 38 - def
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.codeline 55 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.code_source_factorsline 58 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.code_source_coefficientline 72 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TreePath.code_sourceline 83 - lemma
OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.pattern_sourceline 99