OAI/NumberTheory/DirichletL/Detector/PrincipalNormalizer.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.ProbePrincipalNormalizer.sourceResidueConstant_positiveline 13 - theorem
OAI.SevenEighths.ProbePrincipalNormalizer.sourceResidueConstant_ne_zeroline 38 - theorem
OAI.SevenEighths.ProbePrincipalNormalizer.signed_source_normalizer_ne_zeroline 49