OAI/NumberTheory/DirichletL/Dictionary/InverseMarkedReferenceReindex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remainingIndexEquiv line 13
  2. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remaining_product_attach line 19
  3. def OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remainingPi line 24
  4. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.sum_remaining_original line 27
  5. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedReference.remainingPolynomial_original_pi line 45