OAI/NumberTheory/DirichletL/Reflection/Shape.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.InverseReflectedPhase.shapeArgumentline 11 - lemma
OAI.SevenEighths.InverseReflectedPhase.shapeArgument_mulline 13 - lemma
OAI.SevenEighths.InverseReflectedPhase.shapeArgument_normline 18 - lemma
OAI.SevenEighths.InverseReflectedPhase.stratumShapeFactor_mulline 24 - lemma
OAI.SevenEighths.InverseReflectedPhase.actual_shape_separationline 34