OAI/NumberTheory/DirichletL/Reflection/Norms.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.InverseReflectedPhase.crossSymbol_normline 16 - theorem
OAI.SevenEighths.InverseReflectedPhase.local_phase_normline 33 - theorem
OAI.SevenEighths.InverseReflectedPhase.markedPrimeScalar_normline 44 - theorem
OAI.SevenEighths.InverseReflectedPhase.residualPrimeScalar_normline 58 - theorem
OAI.SevenEighths.InverseReflectedPhase.residualWithFrozen_normline 72 - theorem
OAI.SevenEighths.InverseReflectedPhase.markedWithFrozen_normline 93