OAI/NumberTheory/OrdinaryCorrelations/HighTrace/EarlierTuple.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.OrdinaryCorrelations.PivotSummation.earlierTupleline 15 - lemma
OAI.OrdinaryCorrelations.PivotSummation.prefix_consline 18 - theorem
OAI.OrdinaryCorrelations.PivotSummation.triangular_product_sumline 25