OAI/NumberTheory/DirichletL/Detector/CentralCubeNorm.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.ProbeHighRowFamily.cubeArithmeticSum_normline 14 - theorem
OAI.SevenEighths.ProbeHighRowFamily.actual_common_cube_normline 32 - theorem
OAI.SevenEighths.ProbeHighRowFamily.actual_common_cube_aggregate_normline 104