OAI/NumberTheory/DirichletL/Reflection/FrozenNorms.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.InverseReflectedPhase.frozenCofactorCharacter_cross_normline 13 - lemma
OAI.SevenEighths.InverseReflectedPhase.frozenCofactorCharacter_product_normline 30 - lemma
OAI.SevenEighths.InverseReflectedPhase.frozenPrimeScalar_normline 42 - lemma
OAI.SevenEighths.InverseReflectedPhase.frozenCore_normline 54 - lemma
OAI.SevenEighths.InverseReflectedPhase.sourceFrozenPhase_normline 66