OAI/NumberTheory/DirichletL/Inversion/ReflectedNormalization.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.InverseReflectedNormalization.outsideScalarline 11 - theorem
OAI.SevenEighths.InverseReflectedNormalization.smallScalar_rpowline 15 - theorem
OAI.SevenEighths.InverseReflectedNormalization.outsideScalar_squareline 32 - theorem
OAI.SevenEighths.InverseReflectedNormalization.row_shapeline 42 - theorem
OAI.SevenEighths.InverseReflectedNormalization.cubic_shapeline 50 - theorem
OAI.SevenEighths.InverseReflectedNormalization.reflected_exponent_identityline 62 - theorem
OAI.SevenEighths.InverseReflectedNormalization.normalized_hybrid_shapeline 69