OAI/NumberTheory/DirichletL/Dictionary/InverseMarkedReferenceRemaining.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remaining_injectiveline 16 - theorem
OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remaining_moebiusline 25 - def
OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remainingPolynomialline 36 - theorem
OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remainingResidual_eq_polynomialline 44 - theorem
OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.sum_tuple_piline 60 - theorem
OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remainingPolynomial_piline 79