OAI/Combinatorics/Progressions/Linear/NativeRankFamilyConstruction.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.NativeDegreeRankDerivativeData.toFamilyline 18 - theorem
OAI.Erdos3.NativeDegreeRankDerivativeData.toFamily_evalCyclicline 42 - theorem
OAI.Erdos3.NativeDegreeRankDerivativeData.toFamily_correlationline 45